initial definition of soundness theorems

coq/_CoqProject

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

coq/morph.v

@@ -0,0 +1,68 @@
+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,9 +52,10 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
     e1 -->β e1' ->
     (expr_app e1 e2) -->β (expr_app e1' e2)
 
-  | E_App2 : forall e1 e2 e2',
+  | E_App2 : forall v1 e2 e2',
+    (is_value v1) ->
     e2 -->β e2' ->
-    (expr_app e1 e2) -->β (expr_app e1 e2')
+    (expr_app v1 e2) -->β (expr_app v1 e2')
 
   | E_TypApp : forall e e' τ,
     e -->β e' ->

coq/soundness.v

@@ -0,0 +1,83 @@
+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,10 +61,14 @@ 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.
@@ -74,13 +78,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,7 +59,21 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
     Γ |- a \is σ ->
     Γ |- (expr_app f a) \is τ
 
-  | T_Sub : forall Γ x τ τ',
+  | 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 τ τ',
     Γ |- x \is τ ->
     (τ :<= τ') ->
     Γ |- x \is τ'
@@ -68,44 +82,31 @@ 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 τ)
+  | TCompat_Native : forall Γ e τ,
+    (Γ |- e \is τ) ->
+    (Γ |- e \compatible τ)
 
-  | T_CompatLet : forall Γ s (σ:type_term) t τ x,
-    (Γ |- s \compatible σ) ->
+  | TCompat_Let : forall Γ s (σ:type_term) t τ x,
+    (Γ |- s \is σ) ->
+    (context_contains Γ x σ) ->
     (Γ |- 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_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 σ τ,
+  | TCompat_App : forall Γ f a σ τ,
     (Γ |- f \compatible (type_fun σ τ)) ->
     (Γ |- a \compatible σ) ->
     (Γ |- (expr_app f a) \compatible τ)
 
-  | T_CompatImplicitCast : forall Γ h x τ τ',
+  | TCompat_Morph : forall Γ h x τ τ',
     (context_contains Γ h (type_morph τ τ')) ->
     (Γ |- x \compatible τ) ->
     (Γ |- x \compatible τ')
 
-  | T_CompatSub : forall Γ x τ τ',
+  | TCompat_Sub : forall Γ x τ τ',
     (Γ |- x \compatible τ) ->
     (τ ~<= τ') ->
     (Γ |- x \compatible τ')
@@ -117,12 +118,17 @@ 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.
@@ -135,11 +141,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_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
+  apply T_Descend with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
   apply T_TypeAbs.
   apply T_Abs.
   apply H.
@@ -156,12 +162,16 @@ 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_Sub with (τ:=[∀"T",∀"U",(%"T"%->%"U"%->%"U"%)]) (τ':=[∀"S",∀"T",(%"S"%->%"T"%->%"T"%)]).
+  apply T_Descend with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
   apply T_TypeAbs, T_TypeAbs, T_Abs.
   apply H.
   apply T_Abs.
@@ -169,7 +179,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.
@@ -192,20 +202,21 @@ 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 T_CompatTypeAbs.
-  apply T_CompatTypeAbs.
-  apply T_CompatAbs.
+  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.
   apply C_take.
-  apply T_CompatAbs.
+  apply T_Abs.
   apply C_shuffle. apply C_take.
-  apply T_CompatVar.
+  apply T_Var.
   apply C_take.
 Qed.