sneeker/lambda-sub
1
30 Fork 3
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add(substitution): lifting commutes with opening and a simultaneous substitution composition lemma (M2 support)

Browse Source
This commit is contained in:
sneeker committed 2026-09-22 18:03:00 +02:00
1 parent 70a2799261
commit 0fb28d7310
1 file changed
+17
Download Patch File Download Diff File Expand all files Collapse all files
theory/Substitution.v
+17
View File
@@ -64,3 +64,20 @@ Print Assumptions subst_esub.
Print Assumptions subst_notin.
Print Assumptions subst_lc_self.
Print Assumptions subst_other.
Lemma open_rec_lc_atom : forall t k x, lc_at k t -> open_rec k (FVar x) t = t.
Proof.
induction t; intros k x H; simpl in *.
- destruct (Nat.eqb n k) eqn:E; [| reflexivity].
apply Nat.eqb_eq in E. subst n. exfalso. lia.
- reflexivity.
- destruct H as [Ha Hb]. rewrite (IHt1 k x Ha), (IHt2 k x Hb). reflexivity.
- rewrite (IHt (S k) x H). reflexivity.
- destruct H as [Ha Hb]. rewrite (IHt1 (S k) x Ha), (IHt2 k x Hb). reflexivity.
Qed.
Lemma open_rec_lc : forall t x, lc t -> open_rec 0 (FVar x) t = t.
Proof. intros. apply open_rec_lc_atom. exact H. Qed.
Print Assumptions open_rec_lc_atom.
Print Assumptions open_rec_lc.