From 4b76d6a98297c3366089f2a3aef55816bd59d0e9 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 21 Sep 2024 01:05:28 +0200
Subject: [PATCH] improve type-opening lemmas

---
 coq/subst_lemmas_debruijn.v | 112 +++++++++---------------------------
 1 file changed, 26 insertions(+), 86 deletions(-)

diff --git a/coq/subst_lemmas_debruijn.v b/coq/subst_lemmas_debruijn.v
index 77c04c0..62c4ead 100644
--- a/coq/subst_lemmas_debruijn.v
+++ b/coq/subst_lemmas_debruijn.v
@@ -52,21 +52,18 @@ Qed.
 
 
 
-Lemma open_rec_lc_core : forall τ i σ1 j σ2,
+Lemma type_open_lc_core : forall τ i σ1 j σ2,
   i <> j ->
   {i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
-  ({j ~> σ2} τ) = τ.
-
+  ({j ~> σ2} τ) = τ
+.
 Proof with eauto*.
   induction τ;
-  intros i σ1 j σ2 Neq H.
+  intros i σ1 j σ2 Neq H;
+  simpl in *;
+  inversion H;
+  f_equal; eauto.
 
-  (* id *)
-  - reflexivity.
-  
-  (* free var *)
-  - reflexivity.
-  
   (* bound var *)
   - simpl in *.
     destruct (j === n).
@@ -83,97 +80,40 @@ Proof with eauto*.
     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 σ τ,
+(*
+ * opening is idempotent on locally closed types
+ *)
+Lemma type_open_lc : forall k σ τ,
   type_lc τ ->
   ({ k ~> σ } τ) = τ
 .
 Proof.
   intros.
   generalize dependent k.
-  induction H.
-
-  (* id *)
-  - auto.
-
-  (* free var *)
-  - auto.
+  induction H; eauto; simpl in *; intro k.
 
   (* univ *)
-  - simpl.
-    intro k.
-    f_equal.
-    unfold type_open in *.
-    pick fresh x for L.
-    apply open_rec_lc_core with
+  f_equal.
+  unfold type_open in *.
+  pick fresh x for L.
+  apply type_open_lc_core with
       (i := 0) (σ1 := (ty_fvar x))
       (j := S k) (σ2 := σ).
-    trivial.
-    apply eq_sym, H0, Fr.
+  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.
+  (* rest *)
+  all: rewrite IHtype_lc1; rewrite IHtype_lc2; reflexivity.
 Qed.
 
-Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
+
+(*
+ * type substitution distributes over opening
+ *)
+Lemma type_subst_open : forall τ σ1 σ2 x k,
   type_lc σ2 ->
 
   [x ~> σ2] ({k ~> σ1} τ)
@@ -186,7 +126,7 @@ Proof.
   (* free var *)
   - destruct (x == a).
     subst.
-    apply eq_sym, type_open_rec_lc.
+    apply eq_sym, type_open_lc.
     assumption.
     trivial.