coq: reimplement type substitution and alpha conversion in types

coq/equiv.v

@@ -29,6 +29,7 @@
  * rewrite-step of each other, `===` is symmetric and thus `===`
  * satisfies all properties required of an equivalence relation.
  *)
+
 Require Import terms.
 Require Import subst.
 From Coq Require Import Strings.String.
@@ -41,17 +42,55 @@ Module Equiv.
 
 (** Alpha conversion in types *)
 
-Reserved Notation "S '-->α' T" (at level 40).
+Reserved Notation "S '--->α' T" (at level 40).
 Inductive type_conv_alpha : type_term -> type_term -> Prop :=
-  | TEq_Alpha : forall x y t,
+  | TAlpha_Rename : forall x y t t',
-  (type_univ x t) -->α (type_univ y (type_subst x (type_var y) t))
+
-where "S '-->α' T" := (type_conv_alpha S T).
+  (type_subst1 x (type_var y) t t') ->
+  (type_univ x t) --->α (type_univ y t')
+
+  | TAlpha_SubUniv : forall x τ τ',
+    (τ --->α τ') ->
+    (type_univ x τ) --->α (type_univ x τ')
+
+  | TAlpha_SubSpec1 : forall τ1 τ1' τ2,
+    (τ1 --->α τ1') ->
+    (type_spec τ1 τ2) --->α (type_spec τ1' τ2)
+
+  | TAlpha_SubSpec2 : forall τ1 τ2 τ2',
+    (τ2 --->α τ2') ->
+    (type_spec τ1 τ2) --->α (type_spec τ1 τ2')
+
+  | TAlpha_SubFun1 : forall τ1 τ1' τ2,
+    (τ1 --->α τ1') ->
+    (type_fun τ1 τ2) --->α (type_fun τ1' τ2)
+
+  | TAlpha_SubFun2 : forall τ1 τ2 τ2',
+    (τ2 --->α τ2') ->
+    (type_fun τ1 τ2) --->α (type_fun τ1 τ2')
+
+  | TAlpha_SubMorph1 : forall τ1 τ1' τ2,
+    (τ1 --->α τ1') ->
+    (type_morph τ1 τ2) --->α (type_morph τ1' τ2)
+
+  | TAlpha_SubMorph2 : forall τ1 τ2 τ2',
+    (τ2 --->α τ2') ->
+    (type_morph τ1 τ2) --->α (type_morph τ1 τ2')
+
+  | TAlpha_SubLadder1 : forall τ1 τ1' τ2,
+    (τ1 --->α τ1') ->
+    (type_ladder τ1 τ2) --->α (type_ladder τ1' τ2)
+
+  | TAlpha_SubLadder2 : forall τ1 τ2 τ2',
+    (τ2 --->α τ2') ->
+    (type_ladder τ1 τ2) --->α (type_ladder τ1 τ2')
+
+where "S '--->α' T" := (type_conv_alpha S T).
 
 (** Alpha conversion is symmetric *)
-
 Lemma type_alpha_symm :
   forall σ τ,
-  (σ -->α τ) -> (τ -->α σ).
+  (σ --->α τ) -> (τ --->α σ).
 Proof.
  (* TODO *)
 Admitted.
@@ -179,8 +218,8 @@ Inductive type_eq : type_term -> type_term -> Prop :=
     y === z ->
     x === z
 
-  | TEq_Rename : forall x y,
+  | TEq_Alpha : forall x y,
-    x -->α y ->
+    x --->α y ->
     x === y
 
   | TEq_Distribute : forall x y,
@@ -196,7 +235,7 @@ where "S '===' T" := (type_eq S T).
 
 
 (** Symmetry of === *)
-Lemma type_eq_is_symmetric :
+Lemma TEq_Symm :
   forall x y,
   (x === y) -> (y === x).
 Proof.
@@ -210,7 +249,7 @@ Proof.
   apply IHtype_eq1.
 
   apply type_alpha_symm in H.
-  apply TEq_Rename.
+  apply TEq_Alpha.
   apply H.
 
   apply TEq_Condense.
@@ -268,18 +307,21 @@ Proof.
   intros τ H.
   induction τ.
 
-  left.
-  apply FlatUnit.
-  
   left.
   apply FlatId.
   
   left.
   apply FlatVar.
-
+(*
   left.
-  apply FlatNum.
+  apply IHτ1 in H.
+  apply FlatFun.
+  apply H.
+  destruct H.
+  destruct H.
   
+  apply IHτ1.
+*)
   admit.
   admit.
   admit.

coq/subst.v

@@ -1,9 +1,62 @@
-From Coq Require Import Strings.String.
+ From Coq Require Import Strings.String.
 Require Import terms.
 
 Include Terms.
 
 Module Subst.
+
+(* Type Variable "x" is a free variable in type *)
+Inductive type_var_free (x:string) : type_term -> Prop :=
+  | TFree_Var :
+    (type_var_free x (type_var x))
+
+  | TFree_Ladder : forall τ1 τ2,
+    (type_var_free x τ1) ->
+    (type_var_free x τ2) ->
+    (type_var_free x (type_ladder τ1 τ2))
+
+  | TFree_Fun : forall τ1 τ2,
+    (type_var_free x τ1) ->
+    (type_var_free x τ2) ->
+    (type_var_free x (type_fun τ1 τ2))
+
+  | TFree_Morph : forall τ1 τ2,
+    (type_var_free x τ1) ->
+    (type_var_free x τ2) ->
+    (type_var_free x (type_morph τ1 τ2))
+
+  | TFree_Spec : forall τ1 τ2,
+    (type_var_free x τ1) ->
+    (type_var_free x τ2) ->
+    (type_var_free x (type_spec τ1 τ2))
+
+  | TFree_Univ : forall y τ,
+    ~(y = x) ->
+    (type_var_free x τ) ->
+    (type_var_free x (type_univ y τ))
+.
+
+
+Open Scope ladder_type_scope.
+Example ex_type_free_var1 :
+  (type_var_free "T" (type_univ "U" (type_var "T")))
+.
+Proof.
+  apply TFree_Univ.
+  easy.
+  apply TFree_Var.
+Qed.
+
+Open Scope ladder_type_scope.
+Example ex_type_free_var2 :
+  ~(type_var_free "T" (type_univ "T" (type_var "T")))
+.
+Proof.
+  intro H.
+  inversion H.
+  contradiction.
+Qed.
+
 (* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
 Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
   match t0 with
@@ -15,6 +68,44 @@ Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
   | t => t
   end.
 
+Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop :=
+  | TSubst_VarReplace :
+    (type_subst1 x σ (type_var x) σ)
+
+  | TSubst_VarKeep : forall y,
+    ~(x = y) ->
+    (type_subst1 x σ (type_var y) (type_var y))
+
+  | TSubst_UnivReplace : forall y τ τ',
+    ~(x = y) ->
+    ~(type_var_free y σ) ->
+    (type_subst1 x σ τ τ') ->
+    (type_subst1 x σ (type_univ y τ) (type_univ y τ'))
+
+  | TSubst_Id : forall n,
+    (type_subst1 x σ (type_id n) (type_id n))
+
+  | TSubst_Spec : forall τ1 τ2 τ1' τ2',
+    (type_subst1 x σ τ1 τ1') ->
+    (type_subst1 x σ τ2 τ2') ->
+    (type_subst1 x σ (type_spec τ1 τ2) (type_spec τ1' τ2'))
+
+  | TSubst_Fun : forall τ1 τ1' τ2 τ2',
+    (type_subst1 x σ τ1 τ1') ->
+    (type_subst1 x σ τ2 τ2') ->
+    (type_subst1 x σ (type_fun τ1 τ2) (type_fun τ1' τ2'))
+
+  | TSubst_Morph : forall τ1 τ1' τ2 τ2',
+    (type_subst1 x σ τ1 τ1') ->
+    (type_subst1 x σ τ2 τ2') ->
+    (type_subst1 x σ (type_morph τ1 τ2) (type_morph τ1' τ2'))
+
+  | TSubst_Ladder : forall τ1 τ1' τ2 τ2',
+    (type_subst1 x σ τ1 τ1') ->
+    (type_subst1 x σ τ2 τ2') ->
+    (type_subst1 x σ (type_ladder τ1 τ2) (type_ladder τ1' τ2'))
+.
+
 (* scoped variable substitution, replaces free occurences of v with n in expression e *)
 Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
   match e0 with