coq/_CoqProject

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

coq/bbencode.v

@@ -55,7 +55,12 @@ Definition bb_succ : expr_term :=
                     (expr_var "z")))))))).
 
 Definition e1 : expr_term :=
-  (expr_let "bb-zero" bb_zero
+  (expr_let "bb-zero" (type_ladder (type_id "ℕ")
+                        (type_ladder (type_id "BBNat")
+                          (type_univ "α"
+                            (type_fun (type_fun (type_var "α") (type_var "α"))
+                              (type_fun (type_var "α") (type_var "α"))))))
+                       bb_zero
                        (expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
   ).
 

coq/context.v

@@ -1,21 +0,0 @@
-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,100 +3,66 @@ Require Import terms.
 Require Import subst.
 Require Import equiv.
 Require Import subtype.
-Require Import context.
+Require Import typing.
 
 Include Terms.
 Include Subst.
 Include Equiv.
 Include Subtype.
-Include Context.
+Include Typing.
 
 Module Morph.
 
-(* Given a context, there is a morphism path from τ to τ' *)
-Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
 
-Inductive morphism_path : context -> type_term -> type_term -> Prop :=
+Reserved Notation "Γ '|-' '[[' e ']]' '=' t"  (at level 101, e at next level, t at level 0).
-  | M_Sub : forall Γ τ τ',
-    (τ :<= τ') ->
-    (Γ |- τ ~> τ')
 
-  | M_Single : forall Γ h τ τ',
+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))
 
-  | M_Chain : forall Γ τ τ' τ'',
+  | Expand_Otherwise : forall Γ e,
-    (Γ |- τ ~> τ') ->
+    (Γ |- [[ e ]] = e)
-    (Γ |- τ' ~> τ'') ->
-    (Γ |- τ ~> τ'')
 
-  | M_Lift : forall Γ σ τ τ',
+  | Expand_App : forall Γ f f' a a' σ τ,
-    (Γ |- τ ~> τ') ->
+    (Γ |- f \compatible (type_fun σ τ)) ->
-    (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))
+    (Γ |- a \compatible σ) ->
+    (Γ |- [[ f ]] = f') ->
+    (Γ |- [[ a ]] = a') ->
+    (Γ |- [[ (expr_app f a) ]] = (expr_app f a'))
 
-  | M_MapSeq : forall Γ τ τ',
+where "Γ '|-' '[[' e ']]' '=' t" := (expand_morphisms Γ e t).
-    (Γ |- τ ~> τ') ->
-    (Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))
-
-where "Γ '|-' s '~>' t" := (morphism_path Γ s t).
 
 
-Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
+(* For every well-typed term, there is an expanded exactly typed term *)
-  | Translate_Subtype : forall Γ τ τ',
+Lemma well_typed_is_expandable :
-    (τ :<= τ') ->
+  forall (e:expr_term),
-    (translate_morphism_path Γ τ τ'
+  (is_well_typed e) ->
-        (expr_morph "x" τ (expr_var "x")))
+  exists Γ e', (expand_morphisms Γ e e') -> (is_exactly_typed e')
-
-  | Translate_Lift : forall Γ σ τ τ' m,
-    (Γ |- τ ~> τ') ->
-    (translate_morphism_path Γ τ τ' m) ->
-    (translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
-        (expr_morph "x" (type_ladder σ τ)
-          (expr_ascend (type_ladder σ τ') (expr_app m (expr_descend τ (expr_var "x"))))))
-
-  | Translate_Single : forall Γ h τ τ',
-    (context_contains Γ h (type_morph τ τ')) ->
-    (translate_morphism_path Γ τ τ' (expr_var h))
-
-  | Translate_Chain : forall Γ τ τ' τ'' m1 m2,
-    (translate_morphism_path Γ τ τ' m1) -> 
-    (translate_morphism_path Γ τ' τ'' m2) ->
-    (translate_morphism_path Γ τ τ''
-      (expr_morph "x" τ (expr_app m2 (expr_app m1 (expr_var "x")))))
-
-  | Translate_MapSeq : forall Γ τ τ' m,
-    (translate_morphism_path Γ τ τ' m) ->
-    (translate_morphism_path Γ
-      (type_spec (type_id "Seq") τ)
-      (type_spec (type_id "Seq") τ')
-      (expr_morph "xs"
-        (type_spec (type_id "Seq") τ)
-        (expr_app (expr_app (expr_ty_app (expr_ty_app
-          (expr_var "map") τ) τ') m)
-          (expr_var "xs"))))
-.
-
-
-Example morphism_paths :
-  (ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]
-    (ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$"ℝ"$ ->morph $"Angle"$~$"Radians"$~$"ℝ"$ >]
-      ctx_empty))
-
-  |- [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Degrees"$~$"ℝ"$> >]
-  ~> [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Radians"$~$"ℝ"$> >]
 .
 Proof.
-  intros.
+Admitted.
-  apply M_MapSeq.
-  apply M_Lift.
-  apply M_Chain with (τ':=[<$"Angle"$~$"Turns"$~$"ℝ"$>]).
-  apply M_Single with (h:="degrees-to-turns"%string).
-  apply C_take.
 
-  apply M_Single with (h:="turns-to-radians"%string).
-  apply C_shuffle.
-  apply C_take.
-Qed.
 
+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,6 +22,15 @@ 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),
@@ -31,14 +40,32 @@ Proof.
   
 Admitted.
 
-(* reduction step preserves well-typedness *)
+(* reduction step preserves the type *)
-Lemma preservation :
+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 *)

coq/subst.v

@@ -115,7 +115,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
   | expr_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e)
   | expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e)
   | expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a)
-  | expr_let x a e => expr_let x (expr_subst v n a) (expr_subst v n e)
+  | expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e)
   | expr_ascend t e => expr_ascend t (expr_subst v n e)
   | expr_descend t e => expr_descend t (expr_subst v n e)
   end.

coq/terms.v

@@ -25,11 +25,12 @@ Inductive expr_term : Type :=
   | expr_abs   : string -> type_term -> expr_term -> expr_term
   | expr_morph : string -> type_term -> expr_term -> expr_term
   | expr_app : expr_term -> expr_term -> expr_term
-  | expr_let : string -> expr_term -> expr_term -> expr_term
+  | expr_let : string -> type_term -> expr_term -> expr_term -> expr_term
   | expr_ascend : type_term -> expr_term -> expr_term
   | expr_descend : type_term -> expr_term -> expr_term
 .
 
+
 (* TODO
 
 Inductive type_DeBruijn : Type :=
@@ -98,20 +99,11 @@ 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.
+Notation "'λ' x τ '↦' e" := (expr_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
 Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
-  (in custom ladder_expr at level 10, t constr, e custom ladder_expr at level 80) : ladder_expr_scope.
+  (in custom ladder_expr at level 0, t constr, e custom ladder_expr at level 80).
-Notation "'λ' x τ '↦' e" := (expr_abs x τ e)
+
-  (in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
+
-Notation "'λ' x τ '↦morph' e" := (expr_morph x τ e)
-  (in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
-Notation "'let' x ':=' e 'in' t" := (expr_let x e t)
-  (in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
-Notation "e 'as' τ" := (expr_ascend τ e)
-  (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
-Notation "e1 e2" := (expr_app e1 e2)
-  (in custom ladder_expr at level 50) : ladder_expr_scope.
-Notation "'(' e ')'" := e
-  (in custom ladder_expr at level 0) : ladder_expr_scope.
 
 (* EXAMPLES *)
 
@@ -120,7 +112,7 @@ Open Scope ladder_expr_scope.
 
 Check [< ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) >].
 
-Definition polymorphic_identity1 : expr_term := [{ Λ"T" ↦ λ"x"%"T"% ↦ (%"x"%) }].
+Definition polymorphic_identity1 : expr_term := [{ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% }].
 Definition polymorphic_identity2 : expr_term := [{ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% }].
 
 Compute polymorphic_identity1.

coq/typing.v

@@ -6,55 +6,64 @@ 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 σ t τ x,
+  | T_Let : forall Γ s (σ:type_term) t τ x,
     (Γ |- s \is σ) ->
-    ((ctx_assign x σ Γ) |- t \is τ) ->
+    (Γ |- t \is τ) ->
-    (Γ |- (expr_let x s t) \is τ)
+    (Γ |- (expr_let x σ s t) \is τ)
 
-  | T_TypeAbs : forall Γ e τ α,
+  | T_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
     Γ |- e \is τ ->
     Γ |- (expr_ty_abs α e) \is (type_univ α τ)
 
-  | T_TypeApp : forall Γ α e σ τ τ',
+  | T_TypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
     Γ |- e \is (type_univ α τ) ->
-    (type_subst1 α σ τ τ') ->
+    Γ |- (expr_ty_app e σ) \is (type_subst α σ τ)
-    Γ |- (expr_ty_app e σ) \is τ'
 
-  | T_Abs : forall Γ x σ t τ,
+  | T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
-    ((ctx_assign x σ Γ) |- t \is τ) ->
+    (context_contains Γ x σ) ->
-    (Γ |- (expr_abs x σ t) \is (type_fun σ τ))
+    Γ |- 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 τ,
-    ((ctx_assign x σ Γ) |- e \is τ) ->
+    (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 σ τ)
@@ -64,111 +73,84 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
     (τ' :<= τ) ->
     (Γ |- (expr_ascend τ' e) \is τ')
 
-  | T_DescendImplicit : forall Γ x τ τ',
+  | T_Descend : forall Γ x τ τ',
     Γ |- x \is τ ->
     (τ :<= τ') ->
     Γ |- x \is τ'
 
-  | T_Descend : forall Γ x τ τ',
-    Γ |- x \is τ ->
-    (τ :<= τ') ->
-    Γ |- (expr_descend τ' x) \is τ'
-
 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 \is τ
+  Γ |- e \compatible τ
 .
 
-Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
+Definition is_exactly_typed (e:expr_term) : Prop :=
-  | Expand_Var : forall Γ x τ,
+  exists Γ τ,
-    (Γ |- (expr_var x) \is τ) ->
+  Γ |- e \is τ
-    (translate_typing Γ (expr_var x) τ (expr_var x))
-
-  | Expand_Let : forall Γ x e e' t t' σ τ,
-    (Γ |- e \is σ) ->
-    ((ctx_assign x σ Γ) |- t \is τ) ->
-    (translate_typing Γ e σ e') ->
-    (translate_typing (ctx_assign x σ Γ) t τ t') ->
-    (translate_typing Γ (expr_let x e t) τ (expr_let x e' t'))
-
-  | Expand_TypeAbs : forall Γ α e e' τ,
-    (Γ |- e \is τ) ->
-    (translate_typing Γ e τ e') ->
-    (translate_typing Γ
-      (expr_ty_abs α e)
-      (type_univ α τ)
-      (expr_ty_abs α e'))
-
-  | Expand_TypeApp : forall Γ e e' σ α τ,
-    (Γ |- e \is (type_univ α τ)) ->
-    (translate_typing Γ e τ e') ->
-    (translate_typing Γ (expr_ty_app e τ) (type_subst α σ τ) (expr_ty_app e' τ))
-
-  | Expand_Abs : forall Γ x σ e e' τ,
-    ((ctx_assign x σ Γ) |- e \is τ) ->
-    (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
-    (translate_typing (ctx_assign x σ Γ) e τ e') ->
-    (translate_typing Γ (expr_abs x σ e) (type_fun σ τ) (expr_abs x σ e'))
-
-  | Expand_MorphAbs : forall Γ x σ e e' τ,
-    ((ctx_assign x σ Γ) |- e \is τ) ->
-    (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
-    (translate_typing (ctx_assign x σ Γ) e τ e') ->
-    (translate_typing Γ (expr_morph x σ e) (type_morph σ τ) (expr_morph x σ e'))
-
-  | Expand_App : forall Γ f f' a a' m σ τ σ',
-    (Γ |- f \is (type_fun σ τ)) ->
-    (Γ |- a \is σ') ->
-    (Γ |- σ' ~> σ) ->
-    (translate_typing Γ f (type_fun σ τ) f') ->
-    (translate_typing Γ a σ' a') ->
-    (translate_morphism_path Γ σ' σ m) ->
-    (translate_typing Γ (expr_app f a) τ (expr_app f' (expr_app m a')))
-
-  | Expand_MorphFun : forall Γ f f' σ τ,
-    (Γ |- f \is (type_morph σ τ)) ->
-    (Γ |- f \is (type_fun σ τ)) ->
-    (translate_typing Γ f (type_morph σ τ) f') ->
-    (translate_typing Γ f (type_fun σ τ) f')
-
-  | Expand_Ascend : forall Γ e e' τ τ',
-    (Γ |- e \is τ) ->
-    (τ' :<= τ) ->
-    (Γ |- (expr_ascend τ' e) \is τ') ->
-    (translate_typing Γ e τ e') ->
-    (translate_typing Γ (expr_ascend τ' e) τ' (expr_ascend τ' e'))
-
-  | Expand_Descend : forall Γ e e' τ τ',
-    (Γ |- e \is τ) ->
-    (τ :<= τ') ->
-    (Γ |- e \is τ') ->
-    (translate_typing Γ e τ e') ->
-    (translate_typing Γ e τ' e')
 .
 
 (* Examples *)
 
 Example typing1 :
-  ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
+  forall Γ,
+  (context_contains Γ "x" [< %"T"% >]) ->
+  Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
+   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
 Proof.
   intros.
   apply T_TypeAbs.
   apply T_Abs.
+  apply H.
   apply T_Var.
-  apply C_take.
+  apply H.
 Qed.
 
 Example typing2 :
-  ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
+  forall Γ,
+  (context_contains Γ "x" [< %"T"% >]) ->
+  Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
 Proof.
   intros.
-  apply T_DescendImplicit with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
+  apply T_Descend with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
   apply T_TypeAbs.
   apply T_Abs.
+  apply H.
   apply T_Var.
-  apply C_take.
+  apply H.
 
   apply TSubRepr_Refl.
   apply TEq_Alpha.
@@ -179,18 +161,22 @@ Proof.
 Qed.
 
 Example typing3 :
-  ctx_empty |- [{
+  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_DescendImplicit 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.
-  apply T_Var.
+  apply H0.
-  apply C_take.
+  apply T_Var, H0.
 
   apply TSubRepr_Refl.
   apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ).
@@ -214,70 +200,24 @@ Proof.
   apply TSubst_VarReplace.
 Qed.
 
+
 Example typing4 : (is_well_typed
   [{ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% }]
 ).
 Proof.
   unfold is_well_typed.
-  exists ctx_empty.
+  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_Abs.
-  apply T_Var.
-  apply C_shuffle, C_take.
-Qed.
-
-Open Scope ladder_expr_scope.
-
-Example typing5 : (is_well_typed
-  [{
-    let "deg2turns" :=
-       (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
-                ↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$~$"ℝ"$))
-    in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$~$"ℝ"$) )
-  }]
-).
-Proof.
-  unfold is_well_typed.
-  exists (ctx_assign "60" [< $"ℝ"$ >]
-          (ctx_assign "360" [< $"ℝ"$ >]
-          (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
-              ctx_empty))).
-  exists [< $"Angle"$~$"Turns"$~$"ℝ"$ >].
-  apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]).
-  apply T_MorphAbs.
-  apply T_Ascend with (τ:=[< $"ℝ"$ >]).
-  apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
-  apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
-  apply T_Var.
-  apply C_shuffle. apply C_shuffle. apply C_shuffle. apply C_take.
-  apply T_DescendImplicit with (τ := [< $"Angle"$~$"Degrees"$~$"ℝ"$ >]).
-  apply T_Var.
-  apply C_take.
-  apply TSubRepr_Ladder. apply TSubRepr_Ladder.
-  apply TSubRepr_Refl. apply TEq_Refl.
-  apply M_Sub.
-  apply TSubRepr_Refl. apply TEq_Refl.
-  apply T_Var.
-  apply C_shuffle, C_shuffle, C_take.
-  apply M_Sub.
-  apply TSubRepr_Refl.
-  apply TEq_Refl.
-  apply TSubRepr_Ladder, TSubRepr_Ladder, TSubRepr_Refl.
-  apply TEq_Refl.
-  apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
-  apply T_MorphFun.
-  apply T_Var.
-  apply C_take.
-  apply T_Ascend with (τ:=[<$"ℝ"$>]).
-  apply T_Var.
   apply C_shuffle. apply C_take.
-  apply TSubRepr_Ladder.
+  apply T_Var.
-  apply TSubRepr_Ladder.
+  apply C_take.
-  apply TSubRepr_Refl. apply TEq_Refl.
-  apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
 Qed.
 
 End Typing.

paper/main.tex

@@ -518,23 +518,17 @@ while preserving its semantics.
 \end{enumerate}
 \end{example}
 
-\subsubsection{Typing Context}
+\subsubsection{Inference of Expression Types}
 
 As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\)
 is a finite mapping which assigns variables \(\metavariable{x_i} \in \exprvars\) to types \(\metavariable{\tau_i} \in \nonterm{T}\).
-
+Using the inference rules given in \ref{def:typerules}, further typing-judgements
-%Using the inference rules given in \ref{def:pathrules} \ref{def:typerules}, further typing-judgements
+of the form \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)"
-%of the form \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)"
+can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
-%can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
-
-\subsubsection{Morphism Graph}
-Every typing context \(\Gamma\) implies a \emph{Morphism Graph}, a directed graph whose vertices are types
-and the edges represent a type-transformations, as defined by morphisms.
-A type \(\metavariable{\tau}\) can be implicitly coerced into a type \(\metavariable{\tau'}\),
-provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\),
-written as \(\Gamma  \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\).
 
 \begin{definition}[Morphism Paths]
+Given a typing context \(\Gamma\), any type \(\metavariable{\tau}\) can be transformed into \(\metavariable{\tau'}\), provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\), written as \(\Gamma  \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\).
+
 \label{def:pathrules}
 \begin{mathpar}
 
@@ -789,20 +783,6 @@ D_1
 \and
 
 
-\Big{\llbracket}
-	\inferrule[T-MorphAbs]{
-		D_1 :: \Gamma,\metavariable{x}:\metavariable{\tau} \vdash \metavariable{e} : \metavariable{\tau'} \\
-		\metavariable{\tau} \precsim \metavariable{\tau'}
-	}{
-        \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_\text{morph}}\metavariable{\tau'}
-	}
-\Big{\rrbracket} = 
-\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau}
-\exprterminal{\mapsto_\text{morph}} \Big{\llbracket}D_1\Big{\rrbracket}
-\and
-
-
-
 \Big{\llbracket}
 	\inferrule[T-App]{
 		D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
@@ -928,14 +908,13 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
 	
 	\inferrule[E-AppLamAscribe]{
 	}{
-		\exprterminal{(( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
+		\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
 		\exprterminal{\text{ as }}
 		\typeterminal{\metavariable{\tau}}
-		\exprterminal{)}
+		\metavariable{e}
-		\metavariable{a}
 		\rightarrow_\beta
-		\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
+		\metavariable{v}
-		\metavariable{a}
+		\metavariable{e}
 	}
 \end{mathpar}
 \end{definition}
@@ -945,13 +924,10 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
 
 \begin{lemma}[Preservation]
 \label{lemma:preservation}
-Assume the expression \(\metavariable{e}\) is well typed,
+Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\)
-i.e. there is a type-derivation tree
+for some type \(\metavariable{\tau}\).
-\(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
+Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
-for some type \(\metavariable{\tau}\) and context \(\Gamma\).
+it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
-
-Then forall \(\metavariable{e'}\) with \(\llbracket D \rrbracket \rightarrow_{\beta} \metavariable{e'}\)
-it holds that \(\Gamma \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
 
 \begin{proof}
 \todo{}
@@ -960,31 +936,38 @@ it holds that \(\Gamma \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
 
 \begin{lemma}[Progress]
 \label{lemma:progress}
-Assume the expression \(\metavariable{e}\) is well typed,
+If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\),
-i.e. there is a type-derivation tree
+then either \(\metavariable{e}\) is a value
-\(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
+or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
-for some type \(\metavariable{\tau}\) and context \(\Gamma\).
-
-Then either \(\metavariable{e}\) is a value
-or there exists some \(\metavariable{e'}\) such that \(\llbracket D \rrbracket \rightarrow_{\beta} \metavariable{e'}\)
 
 \begin{proof}
 \todo{}
 \end{proof}
 \end{lemma}
 
-\begin{theorem}[Soundness]
+\begin{theorem}[Syntactic Type Soundness]
-\label{theorem:semantic-soundness}
+\label{theorem:syntactic-soundness}
-No well-typed expression is stuck.
+No syntactically well-typed expression is stuck.
 
-Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\metavariable{\tau}\).
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\metavariable{\tau}\).
+Then it never occurs that \(\metavariable{e} \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
+
+\begin{proof}
+Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
+\end{proof}
+\end{theorem}
+
+\begin{theorem}[Semantic Type Soundness]
+\label{theorem:semantic-soundness}
+No semantically well-typed expression is stuck.
+
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
 Then it never occurs that \(\llbracket D \rrbracket \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
 
 \begin{proof}
-\todo{}
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
-%Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\approx\metavariable{\tau}\).
+By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
-%By \ref{lemma:translation}, \(\Gamma \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
+and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
-%and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
 \end{proof}
 \end{theorem}