coq/equiv.v

@@ -29,7 +29,6 @@
  * 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.
@@ -42,55 +41,17 @@ 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 :=
-  | 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).
+  | 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).
 
 (** Alpha conversion is symmetric *)
+
 Lemma type_alpha_symm :
   forall σ τ,
-  (σ --->α τ) -> (τ --->α σ).
+  (σ -->α τ) -> (τ -->α σ).
 Proof.
  (* TODO *)
 Admitted.
@@ -218,8 +179,8 @@ Inductive type_eq : type_term -> type_term -> Prop :=
     y === z ->
     x === z
 
-  | TEq_Alpha : forall x y,
-    x --->α y ->
+  | TEq_Rename : forall x y,
+    x -->α y ->
     x === y
 
   | TEq_Distribute : forall x y,
@@ -235,7 +196,7 @@ where "S '===' T" := (type_eq S T).
 
 
 (** Symmetry of === *)
-Lemma TEq_Symm :
+Lemma type_eq_is_symmetric :
   forall x y,
   (x === y) -> (y === x).
 Proof.
@@ -249,7 +210,7 @@ Proof.
   apply IHtype_eq1.
 
   apply type_alpha_symm in H.
-  apply TEq_Alpha.
+  apply TEq_Rename.
   apply H.
 
   apply TEq_Condense.
@@ -263,7 +224,9 @@ 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) ->
@@ -306,22 +269,19 @@ Lemma lnf_shape :
 Proof.
   intros τ H.
   induction τ.
-
+  
+  left.
+  apply FlatUnit.
+  
   left.
   apply FlatId.
   
   left.
   apply FlatVar.
-(*
+
   left.
-  apply IHτ1 in H.
-  apply FlatFun.
-  apply H.
-  destruct H.
-  destruct H.
-  
-  apply IHτ1.
-*)
+  apply FlatNum.
+
   admit.
   admit.
   admit.
@@ -335,11 +295,22 @@ 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).
@@ -371,11 +342,11 @@ Admitted.
  *)
 
 Example example_flat_type :
-    (type_is_flat (type_spec (type_id "PosInt") (type_id "10"))).
+    (type_is_flat (type_spec (type_id "PosInt") (type_num 10))).
 Proof.
     apply FlatApp.
     apply FlatId.
-    apply FlatId.
+    apply FlatNum.
 Qed.
 
 Example example_lnf_type :

coq/subst.v

@@ -1,62 +1,9 @@
- 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
@@ -68,44 +15,6 @@ 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,8 +8,10 @@ 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,18 +4,11 @@
 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
@@ -59,68 +52,22 @@ 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_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 τ')
+  | T_Compatible : forall Γ x τ,
+    (Γ |- x \is τ) ->
+    (Γ |- x \compatible τ)
 
 where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
 
-
-(* Examples *)
-
-
 Example typing1 :
   forall Γ,
-  (context_contains Γ "x" [ %"T"% ]) ->
-  Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"T", %"T"% -> %"T"% ].
-   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
+  (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"))).
 Proof.
   intros.
   apply T_TypeAbs.
@@ -128,64 +75,15 @@ Proof.
   apply H.
   apply T_Var.
   apply H.
-Qed.
+Admitted.
 
 Example typing2 :
-  forall Γ,
-  (context_contains Γ "x" [ %"T"% ]) ->
-  Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
-   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
+  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"))).
 Proof.
-  intros.
-  apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
   apply T_TypeAbs.
   apply T_Abs.
-  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.
+  
+Admitted.
 
 End Typing.