coq/_CoqProject

@@ -4,7 +4,6 @@ equiv.v
 subst.v
 subtype.v
 typing.v
-morph.v
 smallstep.v
-soundness.v
 bbencode.v
+

coq/morph.v

@@ -1,68 +0,0 @@
-From Coq Require Import Strings.String.
-Require Import terms.
-Require Import subst.
-Require Import equiv.
-Require Import subtype.
-Require Import typing.
-
-Include Terms.
-Include Subst.
-Include Equiv.
-Include Subtype.
-Include Typing.
-
-Module Morph.
-
-
-Reserved Notation "Γ '|-' '[[' e ']]' '=' t"  (at level 101, e at next level, t at level 0).
-
-Inductive expand_morphisms : context -> expr_term -> expr_term -> Prop :=
-
-  | Expand_Transform : forall Γ e h τ τ',
-    (context_contains Γ h (type_morph τ τ')) ->
-    (Γ |- e \is τ) ->
-    (Γ |- [[ e ]] = (expr_app (expr_var h) e))
-
-  | Expand_Otherwise : forall Γ e,
-    (Γ |- [[ e ]] = e)
-
-  | Expand_App : forall Γ f f' a a' σ τ,
-    (Γ |- f \compatible (type_fun σ τ)) ->
-    (Γ |- a \compatible σ) ->
-    (Γ |- [[ f ]] = f') ->
-    (Γ |- [[ a ]] = a') ->
-    (Γ |- [[ (expr_app f a) ]] = (expr_app f a'))
-
-where "Γ '|-' '[[' e ']]' '=' t" := (expand_morphisms Γ e t).
-
-
-(* For every well-typed term, there is an expanded exactly typed term *)
-Lemma well_typed_is_expandable :
-  forall (e:expr_term),
-  (is_well_typed e) ->
-  exists Γ e', (expand_morphisms Γ e e') -> (is_exactly_typed e')
-.
-Proof.
-Admitted.
-
-
-Example expand1 :
-  (ctx_assign "morph-radix"
-      [< <%"PosInt"% %"16"%> ->morph <%"PosInt"% %"10"%> >]
-  (ctx_assign "fn-decimal"
-      [< <%"PosInt"% %"10"%> -> <%"PosInt"% %"10"%> >]
-  (ctx_assign "x"
-      [< <%"PosInt"% %"16"%> >]
-   ctx_empty)))
-
-  |- [[ (expr_app (expr_var "fn-decimal") (expr_var "x")) ]]
-
-  =  (expr_app (expr_var "fn-decimal")
-      (expr_app (expr_var "morph-radix") (expr_var "x")))
-.
-Proof.
-  apply Expand_App with (f':=(expr_var "fn-decimal")) (σ:=[< < %"PosInt"% %"10"% > >]) (τ:=[< < %"PosInt"% %"10"% > >]).
-  apply TCompat_Native.
-Admitted.
-
-End Morph.

coq/smallstep.v

@@ -52,10 +52,9 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
     e1 -->β e1' ->
     (expr_app e1 e2) -->β (expr_app e1' e2)
 
-  | E_App2 : forall v1 e2 e2',
-    (is_value v1) ->
+  | E_App2 : forall e1 e2 e2',
     e2 -->β e2' ->
-    (expr_app v1 e2) -->β (expr_app v1 e2')
+    (expr_app e1 e2) -->β (expr_app e1 e2')
 
   | E_TypApp : forall e e' τ,
     e -->β e' ->

coq/soundness.v

@@ -1,83 +0,0 @@
-From Coq Require Import Strings.String.
-Require Import terms.
-Require Import subst.
-Require Import equiv.
-Require Import subtype.
-Require Import smallstep.
-Require Import typing.
-
-Include Terms.
-Include Subst.
-Include Equiv.
-Include Subtype.
-Include Smallstep.
-Include Typing.
-
-
-Module Soundness.
-
-(* e is stuck when it is neither a value, nor can it be reduced *)
-Definition is_stuck (e:expr_term) : Prop :=
-  ~(is_value e) ->
-  ~(exists e', e -->β e')
-.
-
-(* every exactly typed term is not stuck *)
-Lemma exact_progress :
-  forall (e:expr_term),
-  (is_exactly_typed e) -> ~(is_stuck e)
-.
-Proof.
-
-Admitted.
-
-(* every well typed term is not stuck *)
-Lemma progress :
-  forall (e:expr_term),
-  (is_well_typed e) -> ~(is_stuck e)
-.
-Proof.
-  
-Admitted.
-
-(* reduction step preserves the type *)
-Lemma exact_preservation :
-  forall Γ e e' τ,
-  (Γ |- e \is τ) ->
-  (e -->β e') ->
-  (Γ |- e' \is τ)
-.
-Proof.
-(*
-  intros.
-  generalize dependent e'.
-  induction H.
-  intros e' I.
-  inversion I.
-  *)
-Admitted.
-
-
-(* reduction step preserves well-typedness *)
-Lemma preservation :
-  forall Γ e e' τ,
-  (Γ |- e \compatible τ) ->
-  (e -->β e') ->
-  (Γ |- e' \compatible τ)
-.
-Proof.
-Admitted.
-
-(* every well-typed expression can be reduced to a value *)
-Theorem soundness :
-  forall (e:expr_term),
-  (is_well_typed e) ->
-  (exists e', e -->β* e' /\ (is_value e'))
-.
-Proof.
-  intros.
-  
-Admitted.
-
-End Soundness.
-

coq/subtype.v

@@ -61,14 +61,10 @@ Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
 
 Example sub0 :
-  [<
-       < $"Seq"$ < $"Digit"$ $"10"$ > >
-     ~ < $"Seq"$ $"Char"$ >
-  >]
+  [   < $"Seq"$ < $"Digit"$ $"10"$ > >
+    ~ < $"Seq"$ $"Char"$ > ]
 :<=
-  [<
-       < $"Seq"$ $"Char"$ >
-  >]
+  [   < $"Seq"$ $"Char"$ > ]
 .
 Proof.
   apply TSubRepr_Ladder.
@@ -78,13 +74,13 @@ Qed.
 
 
 Example sub1 :
-    [< < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > >]
-:<= [< < $"Seq"$ $"Char"$ > >]
+    [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ]
+:<= [ < $"Seq"$ $"Char"$ > ]
 .
 Proof.
-  set [< < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > >].
-	set [< < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > >].
-	set [< < $"Seq"$ $"Char"$ > >].
+  set [ < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > ].
+	set [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ].
+	set [ < $"Seq"$ $"Char"$ > ].
 	set (t0 === t).
 	set (t :<= t0).
 	set (t :<= t1).

coq/terms.v

@@ -50,7 +50,7 @@ Declare Scope ladder_expr_scope.
 Declare Custom Entry ladder_type.
 Declare Custom Entry ladder_expr.
 
-Notation "[< t >]" := t
+Notation "[ t ]" := t
   (t custom ladder_type at level 80) : ladder_type_scope.
 Notation "'∀' x ',' t" := (type_univ x t)
   (t custom ladder_type at level 80, in custom ladder_type at level 80, x constr).
@@ -69,7 +69,7 @@ Notation "'$' x '$'" := (type_id x%string)
 Notation "'%' x '%'" := (type_var x%string)
   (in custom ladder_type at level 0, x constr) : ladder_type_scope.
 
-Notation "[{ e }]" := e
+Notation "[[ e ]]" := e
   (e custom ladder_expr at level 80) : ladder_expr_scope.
 Notation "'%' x '%'" := (expr_var x%string)
   (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
@@ -84,10 +84,10 @@ Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
 Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
 
-Check [< ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) >].
+Check [ ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) ].
 
-Definition polymorphic_identity1 : expr_term := [{ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% }].
-Definition polymorphic_identity2 : expr_term := [{ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% }].
+Definition polymorphic_identity1 : expr_term := [[ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% ]].
+Definition polymorphic_identity2 : expr_term := [[ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% ]].
 
 Compute polymorphic_identity1.
 

coq/typing.v

@@ -59,21 +59,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
     Γ |- a \is σ ->
     Γ |- (expr_app f a) \is τ
 
-  | T_MorphAbs : forall Γ x σ e τ,
-    (context_contains Γ x σ) ->
-    Γ |- e \is τ ->
-    Γ |- (expr_morph x σ e) \is (type_morph σ τ)
-
-  | T_MorphFun : forall Γ f σ τ,
-    Γ |- f \is (type_morph σ τ) ->
-    Γ |- f \is (type_fun σ τ)
-
-  | T_Ascend : forall Γ e τ τ',
-    (Γ |- e \is τ) ->
-    (τ' :<= τ) ->
-    (Γ |- (expr_ascend τ' e) \is τ')
-
-  | T_Descend : forall Γ x τ τ',
+  | T_Sub : forall Γ x τ τ',
     Γ |- x \is τ ->
     (τ :<= τ') ->
     Γ |- x \is τ'
@@ -82,31 +68,44 @@ where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
 
 Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
-  | TCompat_Native : forall Γ e τ,
-    (Γ |- e \is τ) ->
-    (Γ |- e \compatible τ)
+  | T_CompatVar : forall Γ x τ,
+    (context_contains Γ x τ) ->
+    (Γ |- (expr_var x) \compatible τ)
 
-  | TCompat_Let : forall Γ s (σ:type_term) t τ x,
-    (Γ |- s \is σ) ->
-    (context_contains Γ x σ) ->
+  | 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 α σ τ)
 
-  | TCompat_App : forall Γ f a σ τ,
+  | T_CompatMorphAbs : forall Γ x t τ τ',
+    Γ |- t \compatible τ ->
+    (τ ~<= τ') ->
+    Γ |- (expr_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_abs x σ t) \compatible (type_fun σ τ)
+
+  | T_CompatApp : forall Γ f a σ τ,
     (Γ |- f \compatible (type_fun σ τ)) ->
     (Γ |- a \compatible σ) ->
     (Γ |- (expr_app f a) \compatible τ)
 
-  | TCompat_Morph : forall Γ h x τ τ',
+  | T_CompatImplicitCast : forall Γ h x τ τ',
     (context_contains Γ h (type_morph τ τ')) ->
     (Γ |- x \compatible τ) ->
     (Γ |- x \compatible τ')
 
-  | TCompat_Sub : forall Γ x τ τ',
+  | T_CompatSub : forall Γ x τ τ',
     (Γ |- x \compatible τ) ->
     (τ ~<= τ') ->
     (Γ |- x \compatible τ')
@@ -118,17 +117,12 @@ Definition is_well_typed (e:expr_term) : Prop :=
   Γ |- e \compatible τ
 .
 
-Definition is_exactly_typed (e:expr_term) : Prop :=
-  exists Γ τ,
-  Γ |- e \is τ
-.
-
 (* Examples *)
 
 Example typing1 :
   forall Γ,
-  (context_contains Γ "x" [< %"T"% >]) ->
-  Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
+  (context_contains Γ "x" [ %"T"% ]) ->
+  Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"T", %"T"% -> %"T"% ].
    (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
 Proof.
   intros.
@@ -141,11 +135,11 @@ Qed.
 
 Example typing2 :
   forall Γ,
-  (context_contains Γ "x" [< %"T"% >]) ->
-  Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
+  (context_contains Γ "x" [ %"T"% ]) ->
+  Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
 Proof.
   intros.
-  apply T_Descend with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
+  apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
   apply T_TypeAbs.
   apply T_Abs.
   apply H.
@@ -162,16 +156,12 @@ 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"%)
-  >].
+  (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_Descend with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
+  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.
@@ -179,7 +169,7 @@ Proof.
   apply T_Var, H0.
 
   apply TSubRepr_Refl.
-  apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ).
+  apply TEq_Trans with (y:= [∀"S",∀"U",(%"S"%->%"U"%->%"U"%)] ).
   apply TEq_Alpha.
   apply TAlpha_Rename.
   apply TSubst_UnivReplace. discriminate.
@@ -202,21 +192,20 @@ Qed.
 
 
 Example typing4 : (is_well_typed
-  [{ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% }]
+  [[ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% ]]
 ).
 Proof.
   unfold is_well_typed.
-  exists (ctx_assign "x" [< %"T"% >]
-            (ctx_assign "y" [< %"U"% >] ctx_empty)).
-  exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
-  apply TCompat_Native.
-  apply T_TypeAbs.
-  apply T_TypeAbs.
-  apply T_Abs.
+  exists (ctx_assign "x" [%"T"%]
+            (ctx_assign "y" [%"U"%] ctx_empty)).
+  exists [ ∀"T",∀"U",%"T"%->%"U"%->%"T"% ].
+  apply T_CompatTypeAbs.
+  apply T_CompatTypeAbs.
+  apply T_CompatAbs.
   apply C_take.
-  apply T_Abs.
+  apply T_CompatAbs.
   apply C_shuffle. apply C_take.
-  apply T_Var.
+  apply T_CompatVar.
   apply C_take.
 Qed.