D.Dot.examples.syn.syn_lemmas
From D.Dot Require Import syn.
Implicit Types
(L T U : ty) (v : vl) (e : tm) (d : dm) (ds : dms)
(Γ : ctx) (ρ : vls).
Implicit Types
(L T U : ty) (v : vl) (e : tm) (d : dm) (ds : dms)
(Γ : ctx) (ρ : vls).
Here is a manual proof of fv_vabs_inv, with explanations, as
documentation for solve_inv_fv_congruence.
Lemma fv_vabs_inv_manual e n : nclosed_vl (vabs e) n → nclosed e n.+1.
Proof.
rewrite /nclosed_vl /nclosed ⇒ /= Hfv s1 s2 HsEq.
(* From Hfv, we only learn that e.|[up s1] = e.|[up s2], for arbitrary
s1 and s2, but substitutions in our thesis e.|[s1] = e.|[s2] are not
of form up ?. Hence, we rewrite it using decomp_s / decomp_s_vl to
get a substitution of form up ?, then rewrite with e.|[up (stail s1)] = e.|[up (stail s2)] (got from Hfv), and conclude.
*)
rewrite ?(decomp_s _ s1) ?(decomp_s _ s2) ?(decomp_s_vl _ s1) ?(decomp_s_vl _ s2) (eq_n_s_heads HsEq); last lia.
injection (Hfv _ _ (eq_n_s_tails HsEq)); rewritePremises; reflexivity.
Qed.
Proof.
rewrite /nclosed_vl /nclosed ⇒ /= Hfv s1 s2 HsEq.
(* From Hfv, we only learn that e.|[up s1] = e.|[up s2], for arbitrary
s1 and s2, but substitutions in our thesis e.|[s1] = e.|[s2] are not
of form up ?. Hence, we rewrite it using decomp_s / decomp_s_vl to
get a substitution of form up ?, then rewrite with e.|[up (stail s1)] = e.|[up (stail s2)] (got from Hfv), and conclude.
*)
rewrite ?(decomp_s _ s1) ?(decomp_s _ s2) ?(decomp_s_vl _ s1) ?(decomp_s_vl _ s2) (eq_n_s_heads HsEq); last lia.
injection (Hfv _ _ (eq_n_s_tails HsEq)); rewritePremises; reflexivity.
Qed.
The following ones are "direct" lemmas: deduce that an expression is closed
by knowing that its subexpression are closed.