improve type-opening lemmas

coq/subst_lemmas_debruijn.v

@@ -52,20 +52,17 @@ 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 *;
-  (* id *)
+  inversion H;
-  - reflexivity.
+  f_equal; eauto.
-  
-  (* free var *)
-  - reflexivity.
 
   (* bound var *)
   - simpl in *.
@@ -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.
+  induction H; eauto; simpl in *; intro k.
-
-  (* id *)
-  - auto.
-
-  (* free var *)
-  - auto.
 
   (* univ *)
-  - simpl.
+  f_equal.
-    intro k.
+  unfold type_open in *.
-    f_equal.
+  pick fresh x for L.
-    unfold type_open in *.
+  apply type_open_lc_core with
-    pick fresh x for L.
-    apply open_rec_lc_core with
       (i := 0) (σ1 := (ty_fvar x))
       (j := S k) (σ2 := σ).
-    trivial.
+  trivial.
-    apply eq_sym, H0, Fr.
+  apply eq_sym, H0, Fr.
 
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+  (* rest *)
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
+  all: 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 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.