coq: add 'compatible' typing relation

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,
-  (type_univ x t) -->α (type_univ y (type_subst x (type_var y) t))
-where "S '-->α' T" := (type_conv_alpha S T).
+  | TAlpha_Rename : forall x y t 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,
-    x -->α y ->
+  | TEq_Alpha : forall 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.
@@ -224,9 +263,7 @@ Qed.
 
 (** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
 Inductive type_is_flat : type_term -> Prop :=
-  | FlatUnit : (type_is_flat type_unit)
   | FlatVar : forall x, (type_is_flat (type_var x))
-  | FlatNum : forall x, (type_is_flat (type_num x))
   | FlatId : forall x, (type_is_flat (type_id x))
   | FlatApp : forall x y,
     (type_is_flat x) ->
@@ -269,19 +306,22 @@ Lemma lnf_shape :
 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.
@@ -295,22 +335,11 @@ Proof.
   intros.
   destruct t.
 
-  exists type_unit.
-  split. apply TEq_Refl.
-  apply LNF.
-  admit.
-  
   exists (type_id s).
   split. apply TEq_Refl.
   apply LNF.
   admit.
   admit.
-  
-  exists (type_num n).
-  split. apply TEq_Refl.
-  apply LNF.
-  admit.
-  
   admit.
   
   exists (type_univ s t).
@@ -342,11 +371,11 @@ Admitted.
  *)
 
 Example example_flat_type :
-    (type_is_flat (type_spec (type_id "PosInt") (type_num 10))).
+    (type_is_flat (type_spec (type_id "PosInt") (type_id "10"))).
 Proof.
     apply FlatApp.
     apply FlatId.
-    apply FlatNum.
+    apply FlatId.
 Qed.
 
 Example example_lnf_type :

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

coq/terms.v

@@ -8,10 +8,8 @@ Module Terms.
 
 (* types *)
 Inductive type_term : Type :=
-  | type_unit : type_term
   | type_id : string -> type_term
   | type_var : string -> type_term
-  | type_num : nat -> type_term
   | type_fun : type_term -> type_term -> type_term
   | type_univ : string -> type_term -> type_term
   | type_spec : type_term -> type_term -> type_term

coq/typing.v

@@ -4,11 +4,18 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import subst.
+Require Import equiv.
+Require Import subtype.
+
 Include Terms.
 Include Subst.
+Include Equiv.
+Include Subtype.
 
 Module Typing.
 
+(** Typing Derivation *)
+
 Inductive context : Type :=
   | ctx_assign : string -> type_term -> context -> context
   | ctx_empty : context
@@ -52,22 +59,68 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
     Γ |- a \is σ ->
     Γ |- (expr_tm_app f a) \is τ
 
+  | T_Sub : forall Γ x τ τ',
+    Γ |- x \is τ ->
+    (τ :<= τ') ->
+    Γ |- x \is τ'
+
 where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
 
 Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
+  | T_CompatVar : forall Γ x τ,
+    (context_contains Γ x τ) ->
+    (Γ |- (expr_var x) \compatible τ)
 
-  | T_Compatible : forall Γ x τ,
-    (Γ |- x \is τ) ->
-    (Γ |- x \compatible τ)
+  | T_CompatLet : forall Γ s (σ:type_term) t τ x,
+    (Γ |- s \compatible σ) ->
+    (Γ |- t \compatible τ) ->
+    (Γ |- (expr_let x σ s t) \compatible τ)
+
+  | T_CompatTypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
+    Γ |- e \compatible τ ->
+    Γ |- (expr_ty_abs α e) \compatible (type_univ α τ)
+
+  | T_CompatTypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
+    Γ |- e \compatible (type_univ α τ) ->
+    Γ |- (expr_ty_app e σ) \compatible (type_subst α σ τ)
+
+  | T_CompatMorphAbs : forall Γ x t τ τ',
+    Γ |- t \compatible τ ->
+    (τ ~<= τ') ->
+    Γ |- (expr_tm_abs_morph x τ t) \compatible (type_morph τ τ')
+
+  | T_CompatAbs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
+    (context_contains Γ x σ) ->
+    Γ |- t \compatible τ ->
+    Γ |- (expr_tm_abs x σ t) \compatible (type_fun σ τ)
+
+  | T_CompatApp : forall Γ f a σ τ,
+    (Γ |- f \compatible (type_fun σ τ)) ->
+    (Γ |- a \compatible σ) ->
+    (Γ |- (expr_tm_app f a) \compatible τ)
+
+  | T_CompatImplicitCast : forall Γ h x τ τ',
+    (context_contains Γ h (type_morph τ τ')) ->
+    (Γ |- x \compatible τ) ->
+    (Γ |- x \compatible τ')
+
+  | T_CompatSub : forall Γ x τ τ',
+    (Γ |- x \compatible τ) ->
+    (τ ~<= τ') ->
+    (Γ |- x \compatible τ')
 
 where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
 
+
+(* Examples *)
+
+
 Example typing1 :
   forall Γ,
-  (context_contains Γ "x" (type_var "T")) ->
-  Γ |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
-    (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
+  (context_contains Γ "x" [ %"T"% ]) ->
+  Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"T", %"T"% -> %"T"% ].
+   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
 Proof.
   intros.
   apply T_TypeAbs.
@@ -75,15 +128,64 @@ Proof.
   apply H.
   apply T_Var.
   apply H.
-Admitted.
+Qed.
 
 Example typing2 :
-  ctx_empty |- (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \is
-    (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
+  forall Γ,
+  (context_contains Γ "x" [ %"T"% ]) ->
+  Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
+   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
 Proof.
+  intros.
+  apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
   apply T_TypeAbs.
   apply T_Abs.
-  
-Admitted.
+  apply H.
+  apply T_Var.
+  apply H.
+
+  apply TSubRepr_Refl.
+  apply TEq_Alpha.
+  apply TAlpha_Rename.
+  apply TSubst_Fun.
+  apply TSubst_VarReplace.
+  apply TSubst_VarReplace.
+Qed.
+
+Example typing3 :
+  forall Γ,
+  (context_contains Γ "x" [ %"T"% ]) ->
+  (context_contains Γ "y" [ %"U"% ]) ->
+  Γ |- [[ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"y"% ]] \is [ ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) ].
+Proof.
+  intros.
+  apply T_Sub with (τ:=[∀"T",∀"U",(%"T"%->%"U"%->%"U"%)]) (τ':=[∀"S",∀"T",(%"S"%->%"T"%->%"T"%)]).
+  apply T_TypeAbs, T_TypeAbs, T_Abs.
+  apply H.
+  apply T_Abs.
+  apply H0.
+  apply T_Var, H0.
+
+  apply TSubRepr_Refl.
+  apply TEq_Trans with (y:= [∀"S",∀"U",(%"S"%->%"U"%->%"U"%)] ).
+  apply TEq_Alpha.
+  apply TAlpha_Rename.
+  apply TSubst_UnivReplace. discriminate.
+  easy.
+  apply TSubst_Fun.
+  apply TSubst_VarReplace.
+  apply TSubst_Fun.
+  apply TSubst_VarKeep. discriminate.
+  apply TSubst_VarKeep. discriminate.
+
+  apply TEq_Alpha.
+  apply TAlpha_SubUniv.
+  apply TAlpha_Rename.
+  apply TSubst_Fun.
+  apply TSubst_VarKeep. discriminate.
+  apply TSubst_Fun.
+  apply TSubst_VarReplace.
+  apply TSubst_VarReplace.
+Qed.
 
 End Typing.