From c4f4e56fee70e6fb945280e77f98fd2c1bcb185f Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Fri, 20 Sep 2024 19:41:27 +0200
Subject: [PATCH] move subst/opening lemmas to separate file

---
 coq/_CoqProject             |   5 +-
 coq/subst_lemmas_debruijn.v | 197 ++++++++++++++++++++++++++++++++++++
 coq/terms_debruijn.v        | 196 -----------------------------------
 3 files changed, 201 insertions(+), 197 deletions(-)
 create mode 100644 coq/subst_lemmas_debruijn.v

diff --git a/coq/_CoqProject b/coq/_CoqProject
index 8e717ae..ed0946f 100644
--- a/coq/_CoqProject
+++ b/coq/_CoqProject
@@ -5,8 +5,11 @@ FiniteSets.v
 FSetNotin.v
 Atom.v
 Metatheory.v
-terms.v
+
 terms_debruijn.v
+subst_lemmas_debruijn.v
+
+terms.v
 equiv.v
 subst.v
 subtype.v
diff --git a/coq/subst_lemmas_debruijn.v b/coq/subst_lemmas_debruijn.v
new file mode 100644
index 0000000..77c04c0
--- /dev/null
+++ b/coq/subst_lemmas_debruijn.v
@@ -0,0 +1,197 @@
+Require Import terms_debruijn.
+Require Import Atom.
+Require Import Metatheory.
+Require Import FSetNotin.
+
+(*
+ * Substitution has no effect if the variable is not free
+ *)
+Lemma type_subst_fresh : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
+  x `notin` (type_fv τ) ->
+  ([ x ~> σ ] τ) = τ
+.
+Proof.
+  intros.
+  induction τ.
+
+  - reflexivity.
+
+  - unfold type_fv in H.
+    apply AtomSetNotin.elim_notin_singleton in H.
+    simpl.
+    case_eq (x == a).
+    congruence.
+    reflexivity.
+
+  - reflexivity.
+
+  - simpl. rewrite IHτ.
+    reflexivity.
+    apply H.
+
+  - simpl; rewrite IHτ1, IHτ2.
+    reflexivity.
+    simpl type_fv in H; fsetdec.
+    simpl type_fv in H; fsetdec.
+
+  - simpl. rewrite IHτ1, IHτ2.
+    reflexivity.
+    simpl type_fv in H; fsetdec.
+    simpl type_fv in H; fsetdec.
+
+  - simpl. rewrite IHτ1, IHτ2.
+    reflexivity.
+    simpl type_fv in H; fsetdec.
+    simpl type_fv in H; fsetdec.
+
+  - simpl. rewrite IHτ1, IHτ2.
+    reflexivity.
+    simpl type_fv in H; fsetdec.
+    simpl type_fv in H; fsetdec.
+Qed.
+
+
+
+Lemma open_rec_lc_core : forall τ i σ1 j σ2,
+  i <> j ->
+  {i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
+  ({j ~> σ2} τ) = τ.
+
+Proof with eauto*.
+  induction τ;
+  intros i σ1 j σ2 Neq H.
+
+  (* id *)
+  - reflexivity.
+  
+  (* free var *)
+  - reflexivity.
+  
+  (* bound var *)
+  - simpl in *.
+    destruct (j === n).
+    destruct (i === n).
+    3:reflexivity.
+
+    rewrite e,e0 in Neq.
+    contradiction Neq.
+    reflexivity.
+
+    rewrite H,e.
+    simpl.
+    destruct (n===n).
+    reflexivity.
+    contradict n1.
+    reflexivity.
+
+  (* univ *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    apply IHτ with (i:=S i) (j:=S j) (σ1:=σ1).
+    auto.
+    apply H1.
+
+  (* spec *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+  (* func *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+
+  (* morph *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+  (* ladder *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+Qed.
+
+
+Lemma type_open_rec_lc : forall k σ τ,
+  type_lc τ ->
+  ({ k ~> σ } τ) = τ
+.
+Proof.
+  intros.
+  generalize dependent k.
+  induction H.
+
+  (* id *)
+  - auto.
+
+  (* free var *)
+  - auto.
+
+  (* univ *)
+  - simpl.
+    intro k.
+    f_equal.
+    unfold type_open in *.
+    pick fresh x for L.
+    apply open_rec_lc_core with
+      (i := 0) (σ1 := (ty_fvar x))
+      (j := S k) (σ2 := σ).
+    trivial.
+    apply eq_sym, H0, Fr.
+
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+Qed.
+
+Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
+  type_lc σ2 ->
+
+  [x ~> σ2] ({k ~> σ1} τ)
+  =
+  {k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
+Proof.
+  induction τ;
+  intros; simpl; f_equal; auto.
+
+  (* free var *)
+  - destruct (x == a).
+    subst.
+    apply eq_sym, type_open_rec_lc.
+    assumption.
+    trivial.
+
+  (* bound var *)
+  - destruct (k === n).
+    reflexivity.
+    trivial.
+Qed.
diff --git a/coq/terms_debruijn.v b/coq/terms_debruijn.v
index b56f0a1..1e7706f 100644
--- a/coq/terms_debruijn.v
+++ b/coq/terms_debruijn.v
@@ -7,7 +7,6 @@ Local Open Scope nat_scope.
 Require Import Atom.
 Require Import Metatheory.
 Require Import FSetNotin.
-Require Import terms.
 
 Inductive type_DeBruijn : Type :=
   | ty_id : string -> type_DeBruijn
@@ -130,198 +129,3 @@ Fixpoint type_named2debruijn (τ:type_term) {struct τ} : type_DeBruijn :=
 
 Coercion type_named2debruijn : type_term >-> type_DeBruijn.
 *)
-
-
-
-(*
- * Substitution has no effect if the variable is not free
- *)
-Lemma subst_fresh_type : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
-  x `notin` (type_fv τ) ->
-  ([ x ~> σ ] τ) = τ
-.
-Proof.
-  intros.
-  induction τ.
-
-  - reflexivity.
-
-  - unfold type_fv in H.
-    apply AtomSetNotin.elim_notin_singleton in H.
-    simpl.
-    case_eq (x == a).
-    congruence.
-    reflexivity.
-
-  - reflexivity.
-
-  - simpl. rewrite IHτ.
-    reflexivity.
-    apply H.
-
-  - simpl; rewrite IHτ1, IHτ2.
-    reflexivity.
-    simpl type_fv in H; fsetdec.
-    simpl type_fv in H; fsetdec.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    simpl type_fv in H; fsetdec.
-    simpl type_fv in H; fsetdec.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    simpl type_fv in H; fsetdec.
-    simpl type_fv in H; fsetdec.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    simpl type_fv in H; fsetdec.
-    simpl type_fv in H; fsetdec.
-Qed.
-
-
-
-Lemma open_rec_lc_core : forall τ i σ1 j σ2,
-  i <> j ->
-  {i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
-  ({j ~> σ2} τ) = τ.
-
-Proof with eauto*.
-  induction τ;
-  intros i σ1 j σ2 Neq H.
-
-  (* id *)
-  - reflexivity.
-  
-  (* free var *)
-  - reflexivity.
-  
-  (* bound var *)
-  - simpl in *.
-    destruct (j === n).
-    destruct (i === n).
-    3:reflexivity.
-
-    rewrite e,e0 in Neq.
-    contradiction Neq.
-    reflexivity.
-
-    rewrite H,e.
-    simpl.
-    destruct (n===n).
-    reflexivity.
-    contradict n1.
-    reflexivity.
-
-  (* univ *)
-  - simpl in *.
-    inversion H.
-    f_equal.
-    apply IHτ with (i:=S i) (j:=S j) (σ1:=σ1).
-    auto.
-    apply H1.
-
-  (* spec *)
-  - simpl in *.
-    inversion H.
-    f_equal.
-    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
-      auto.
-      apply H1.
-    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
-      auto.
-      apply H2.
-
-  (* func *)
-  - simpl in *.
-    inversion H.
-    f_equal.
-    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
-      auto.
-      apply H1.
-    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
-      auto.
-      apply H2.
-
-
-  (* morph *)
-  - simpl in *.
-    inversion H.
-    f_equal.
-    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
-      auto.
-      apply H1.
-    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
-      auto.
-      apply H2.
-
-  (* ladder *)
-  - simpl in *.
-    inversion H.
-    f_equal.
-    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
-      auto.
-      apply H1.
-    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
-      auto.
-      apply H2.
-
-Qed.
-
-
-Lemma type_open_rec_lc : forall k σ τ,
-  type_lc τ ->
-  ({ k ~> σ } τ) = τ
-.
-Proof.
-  intros.
-  generalize dependent k.
-  induction H.
-
-  (* id *)
-  - auto.
-
-  (* free var *)
-  - auto.
-
-  (* univ *)
-  - simpl.
-    intro k.
-    f_equal.
-    unfold type_open in *.
-    pick fresh x for L.
-    apply open_rec_lc_core with
-      (i := 0) (σ1 := (ty_fvar x))
-      (j := S k) (σ2 := σ).
-    trivial.
-    apply eq_sym, H0, Fr.
-
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-Qed.
-
-Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
-  type_lc σ2 ->
-
-  [x ~> σ2] ({k ~> σ1} τ)
-  =
-  {k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
-Proof.
-  induction τ;
-  intros; simpl; f_equal; auto.
-
-  (* free var *)
-  - destruct (x == a).
-    subst.
-    apply eq_sym, type_open_rec_lc.
-    assumption.
-    trivial.
-
-  (* bound var *)
-  - destruct (k === n).
-    reflexivity.
-    trivial.
-Qed.