coq: move context into separate module, define morphism-path & redefine typing rules

coq/_CoqProject

@@ -3,8 +3,9 @@ terms.v
 equiv.v
 subst.v
 subtype.v
-typing.v
+context.v
 morph.v
+typing.v
 smallstep.v
 soundness.v
 bbencode.v

coq/context.v

@@ -0,0 +1,21 @@
+From Coq Require Import Strings.String.
+Require Import terms.
+Include Terms.
+
+Module Context.
+
+
+Inductive context : Type :=
+  | ctx_assign : string -> type_term -> context -> context
+  | ctx_empty : context
+.
+
+Inductive context_contains : context -> string -> type_term -> Prop :=
+  | C_take : forall (x:string) (X:type_term) (Γ:context),
+    (context_contains (ctx_assign x X Γ) x X)
+  | C_shuffle : forall x X y Y Γ,
+    (context_contains Γ x X) ->
+    (context_contains (ctx_assign y Y Γ) x X).
+
+
+End Context.

coq/morph.v

@@ -3,66 +3,37 @@ Require Import terms.
 Require Import subst.
 Require Import equiv.
 Require Import subtype.
-Require Import typing.
+Require Import context.
 
 Include Terms.
 Include Subst.
 Include Equiv.
 Include Subtype.
-Include Typing.
+Include Context.
 
 Module Morph.
 
+(* Given a context, there is a morphism path from τ to τ' *)
+Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
 
-Reserved Notation "Γ '|-' '[[' e ']]' '=' t"  (at level 101, e at next level, t at level 0).
+Inductive morphism_path : context -> type_term -> type_term -> Prop :=
+  | M_Sub : forall Γ τ τ',
+    (τ :<= τ') ->
+    (Γ |- τ ~> τ')
 
-Inductive expand_morphisms : context -> expr_term -> expr_term -> Prop :=
+  | M_Single : forall Γ h τ τ',
-
-  | Expand_Transform : forall Γ e h τ τ',
     (context_contains Γ h (type_morph τ τ')) ->
-    (Γ |- e \is τ) ->
+    (Γ |- τ ~> τ')
-    (Γ |- [[ e ]] = (expr_app (expr_var h) e))
 
-  | Expand_Otherwise : forall Γ e,
+  | M_Chain : forall Γ τ τ' τ'',
-    (Γ |- [[ e ]] = e)
+    (Γ |- τ ~> τ') ->
+    (Γ |- τ' ~> τ'') ->
+    (Γ |- τ ~> τ'')
 
-  | Expand_App : forall Γ f f' a a' σ τ,
+  | M_MapSeq : forall Γ τ τ',
-    (Γ |- f \compatible (type_fun σ τ)) ->
+    (Γ |- τ ~> τ') ->
-    (Γ |- a \compatible σ) ->
+    (Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))
-    (Γ |- [[ f ]] = f') ->
-    (Γ |- [[ a ]] = a') ->
-    (Γ |- [[ (expr_app f a) ]] = (expr_app f a'))
 
-where "Γ '|-' '[[' e ']]' '=' t" := (expand_morphisms Γ e t).
+where "Γ '|-' s '~>' t" := (morphism_path Γ s t).
 
-
+End Morph.
-(* 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/soundness.v

@@ -22,15 +22,6 @@ Definition is_stuck (e:expr_term) : Prop :=
   ~(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),
@@ -40,32 +31,14 @@ Proof.
   
 Admitted.
 
-(* reduction step preserves the type *)
+(* reduction step preserves well-typedness *)
-Lemma exact_preservation :
+Lemma 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 *)

coq/typing.v

@@ -6,64 +6,56 @@ Require Import terms.
 Require Import subst.
 Require Import equiv.
 Require Import subtype.
+Require Import context.
+Require Import morph.
 
 Include Terms.
 Include Subst.
 Include Equiv.
 Include Subtype.
+Include Context.
+Include Morph.
 
 Module Typing.
 
 (** Typing Derivation *)
 
-Inductive context : Type :=
-  | ctx_assign : string -> type_term -> context -> context
-  | ctx_empty : context
-.
-
-Inductive context_contains : context -> string -> type_term -> Prop :=
-  | C_take : forall (x:string) (X:type_term) (Γ:context),
-    (context_contains (ctx_assign x X Γ) x X)
-  | C_shuffle : forall x X y Y Γ,
-    (context_contains Γ x X) ->
-    (context_contains (ctx_assign y Y Γ) x X).
-
 Reserved Notation "Gamma '|-' x '\is' X"  (at level 101, x at next level, X at level 0).
-Reserved Notation "Gamma '|-' x '\compatible' X"  (at level 101, x at next level, X at level 0).
 
 Inductive expr_type : context -> expr_term -> type_term -> Prop :=
   | T_Var : forall Γ x τ,
     (context_contains Γ x τ) ->
     (Γ |- (expr_var x) \is τ)
 
-  | T_Let : forall Γ s (σ:type_term) t τ x,
+  | T_Let : forall Γ s σ t τ x,
     (Γ |- s \is σ) ->
     (Γ |- t \is τ) ->
     (Γ |- (expr_let x σ s t) \is τ)
 
-  | T_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
+  | T_TypeAbs : forall Γ e τ α,
     Γ |- e \is τ ->
     Γ |- (expr_ty_abs α e) \is (type_univ α τ)
 
-  | T_TypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
+  | T_TypeApp : forall Γ α e σ τ,
     Γ |- e \is (type_univ α τ) ->
     Γ |- (expr_ty_app e σ) \is (type_subst α σ τ)
 
-  | T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
+  | T_Abs : forall Γ x σ t τ,
     (context_contains Γ x σ) ->
     Γ |- t \is τ ->
     Γ |- (expr_abs x σ t) \is (type_fun σ τ)
 
-  | T_App : forall (Γ:context) (f:expr_term) (a:expr_term) (σ:type_term) (τ:type_term),
-    Γ |- f \is (type_fun σ τ) ->
-    Γ |- 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_App : forall Γ f a σ' σ τ,
+    (Γ |- f \is (type_fun σ τ)) ->
+    (Γ |- a \is σ') ->
+    (Γ |- σ' ~> σ) ->
+    (Γ |- (expr_app f a) \is τ)
+
   | T_MorphFun : forall Γ f σ τ,
     Γ |- f \is (type_morph σ τ) ->
     Γ |- f \is (type_fun σ τ)
@@ -80,45 +72,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
 
 where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
-
-Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
-  | TCompat_Native : forall Γ e τ,
-    (Γ |- e \is τ) ->
-    (Γ |- e \compatible τ)
-
-  | TCompat_Let : forall Γ s (σ:type_term) t τ x,
-    (Γ |- s \is σ) ->
-    (context_contains Γ x σ) ->
-    (Γ |- t \compatible τ) ->
-    (Γ |- (expr_let x σ s t) \compatible τ)
-
-  | 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 σ τ,
-    (Γ |- f \compatible (type_fun σ τ)) ->
-    (Γ |- a \compatible σ) ->
-    (Γ |- (expr_app f a) \compatible τ)
-
-  | TCompat_Morph : forall Γ h x τ τ',
-    (context_contains Γ h (type_morph τ τ')) ->
-    (Γ |- x \compatible τ) ->
-    (Γ |- x \compatible τ')
-
-  | TCompat_Sub : forall Γ x τ τ',
-    (Γ |- x \compatible τ) ->
-    (τ ~<= τ') ->
-    (Γ |- x \compatible τ')
-
-where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
-
 Definition is_well_typed (e:expr_term) : Prop :=
-  exists Γ τ,
-  Γ |- e \compatible τ
-.
-
-Definition is_exactly_typed (e:expr_term) : Prop :=
   exists Γ τ,
   Γ |- e \is τ
 .
@@ -200,7 +154,6 @@ Proof.
   apply TSubst_VarReplace.
 Qed.
 
-
 Example typing4 : (is_well_typed
   [{ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% }]
 ).
@@ -209,7 +162,6 @@ Proof.
   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.