syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix expr_open & expr_lc for let case

Browse source
This commit is contained in:
Michael Sippel 2024-09-22 17:34:12 +02:00
parent f0d9a550b6
commit 10cd2f9bc9
2 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
coq/lemmas/subst_lemmas.v
View file

@ -247,6 +247,13 @@ Proof.
discriminate.
apply eq_sym, H1.
assumption.
- unfold expr_open in *.
pick fresh x for L.
apply expr_open_lc_core with (i:=0) (s1:=(ex_fvar x)) (j:=S k) (s2:=s).
discriminate.
apply eq_sym, H1.
assumption.
Qed.
(*

7
coq/terms/debruijn.v
View file

@ -242,7 +242,7 @@ Fixpoint expr_open_rec (k:nat) (t:expr_DeBruijn) (e:expr_DeBruijn) {struct e} :
| ex_morph σ e' => ex_morph σ (expr_open_rec (S k) t e')
| ex_abs σ e' => ex_abs σ (expr_open_rec (S k) t e')
| ex_app e1 e2 => ex_app (expr_open_rec k t e1) (expr_open_rec k t e2)
| ex_let e1 e2 => ex_let (expr_open_rec k t e1) (expr_open_rec k t e2)
| ex_let e1 e2 => ex_let (expr_open_rec k t e1) (expr_open_rec (S k) t e2)
| ex_ascend σ e' => ex_ascend σ (expr_open_rec k t e')
| ex_descend σ e' => ex_descend σ (expr_open_rec k t e')
end.
@ -285,7 +285,10 @@ Inductive expr_lc : expr_DeBruijn -> Prop :=
(forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) e1)) ->
expr_lc (ex_morph σ e1)
| Elc_App : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_app e1 e2)
| Elc_Let : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_let e1 e2)
| Elc_Let : forall e t L,
expr_lc e ->
(forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) t)) ->
expr_lc (ex_let e t)
| Elc_Ascend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_ascend τ e)
| Elc_Descend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_descend τ e)
.