coq/_CoqProject

@@ -1,6 +1,5 @@
 -R . LadderTypes
 terms.v
-terms_debruijn.v
 equiv.v
 subst.v
 subtype.v

coq/bbencode.v

@@ -4,101 +4,77 @@ Require Import terms.
 Require Import subst.
 Require Import smallstep.
 
+Include Terms.
+Include Subst.
+Include Smallstep.
+
 Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
 
-
+(*  let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
-Definition bb_zero : expr_term := [{
+ *                ∀α.(α->α)->α->α
-  (Λ"α" ↦
-  λ"s",(%"α"% -> %"α"%) ↦
-  λ"z",(%"α"%) ↦
-  %"z"%)
-  as $"ℕ"$~$"BBNat"$
-}].
-
-Definition bb_one : expr_term := [{
-  (Λ"α" ↦
-  λ"s",(%"α"% -> %"α"%) ↦
-  λ"z",(%"α"%) ↦
-  (%"s"% %"z"%))
-  as $"ℕ"$~$"BBNat"$
-}].
-
-Definition bb_two : expr_term := [{
-  (Λ"α" ↦
-  λ"s",(%"α"% -> %"α"%) ↦
-  λ"z",(%"α"%) ↦
-  (%"s"% (%"s"% %"z"%)))
-  as $"ℕ"$~$"BBNat"$
-}].
-
-Definition bb_succ : expr_term := [{
-  λ"n",$"ℕ"$
-      ~$"BBNat"$
-      ~(∀"β",(%"β'"%->%"β"%)->%"β"%->%"β"%)
-      ↦
-    ((Λ"α" ↦
-      λ"s",((%"α"%->%"α"%)->%"α"%->%"α"%) ↦
-      λ"z",%"α"% ↦
-      (%"s"% ((%"n"% # %"α"%) %"s"% %"z"%)))
-      as $"ℕ"$~$"BBNat"$)
-}].
-
-Example  example_reduction :
-    (expr_app bb_succ bb_one) -->β* bb_two
-.
-Proof.
-
-  apply Multi_Step with (y:=[{
-    (λ"n",$"ℕ"$
-        ~$"BBNat"$
-        ~(∀"β",(%"β'"%->%"β"%)->%"β"%->%"β"%)
-        ↦
-      ((Λ"α" ↦
-        λ"s",((%"α"%->%"α"%)->%"α"%->%"α"%) ↦
-        λ"z",%"α"% ↦
-        (%"s"% ((%"n"% # %"α"%) %"s"% %"z"%)))
-        as $"ℕ"$~$"BBNat"$))
-
-    (Λ"β" ↦
-     λ"s",(%"β"% -> %"β"%) ↦
-     λ"z",(%"β"%) ↦
-      (%"s"% %"z"%))
-      as $"ℕ"$~$"BBNat"$
-  }]).
-Admitted.
-(*
-  apply E_Alpha.
-  apply E_App2.
-  apply EAlpha_Rename.
-
-  apply Multi_Step with (y:=[{
-      (Λ"α" ↦
-        λ"s",((%"α"%->%"α"%)->%"α"%->%"α"%) ↦
-        λ"z",%"α"% ↦
-        (%"s"% (
-        (((Λ"β" ↦
-          λ"s",(%"β"% -> %"β"%) ↦
-          λ"z",(%"β"%) ↦
-          (%"s"% %"z"%)) as $"ℕ"$~$"BBNat"$)
-          # %"α"%) %"s"% %"z"%)))
-    as $"ℕ"$~$"BBNat"$ }]).
-
-  apply E_AppLam.
-
-  apply Multi_Step with (y:=[{
-      (Λ"α" ↦
-        λ"s",((%"α"%->%"α"%)->%"α"%->%"α"%) ↦
-        λ"z",%"α"% ↦
-        (%"s"% (
-        (((Λ"α'" ↦
-          λ"s",(%"α'"% -> %"α'"%) ↦
-          λ"z",(%"α'"%) ↦
-          (%"s"% %"z"%)) as $"ℕ"$~$"BBNat"$)
-          # %"α"%) %"s"% %"z"%)))
-    as $"ℕ"$~$"BBNat"$ }]).
-  }].
-Qed.
 *)
+Definition bb_zero : expr_term :=
+  (expr_ty_abs "α"
+    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_abs "z" (type_var "α")
+        (expr_var "z")))).
+
+(*  let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
+*)
+Definition bb_one : expr_term :=
+  (expr_ty_abs "α"
+    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_abs "z" (type_var "α")
+        (expr_app (expr_var "s") (expr_var "z"))))).
+
+(*  let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
+*)
+Definition bb_two : expr_term :=
+  (expr_ty_abs "α"
+    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+      (expr_abs "z" (type_var "α")
+        (expr_app (expr_var "s") (expr_app (expr_var "s") (expr_var "z")))))).
+
+
+Definition bb_succ : expr_term :=
+  (expr_abs "n" (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 "α"))))))
+
+       (expr_ascend (type_ladder (type_id "ℕ") (type_id "BBNat"))
+          (expr_ty_abs "α"
+            (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+              (expr_abs "z" (type_var "α")
+                (expr_app (expr_var "s")
+                  (expr_app (expr_app
+                      (expr_ty_app (expr_var "n") (type_var "α"))
+                      (expr_var "s"))
+                    (expr_var "z")))))))).
+
+Definition e1 : expr_term :=
+  (expr_let "bb-zero" bb_zero
+      (expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
+  ).
+
+Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).
+
+Compute (expr_subst "x"
+    (expr_ty_abs "α" (expr_abs "a" (type_var "α") (expr_var "a")))
+    bb_one
+).
+
+Example  example_let_reduction :
+    e1 -->β  (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
+Proof.
+    apply E_Let.
+Qed.
 
 Compute     (expr_app bb_succ bb_zero) -->β bb_one.
+
+Example  example_succ :
+    (expr_app bb_succ bb_zero) -->β bb_one.
+Proof.
+Admitted.

coq/equiv.v

@@ -38,44 +38,46 @@ From Coq Require Import Strings.String.
 
 Reserved Notation "S '--->α' T" (at level 40).
 Inductive type_conv_alpha : type_term -> type_term -> Prop :=
-  | TAlpha_Rename : forall x y t,
+  | TAlpha_Rename : forall x y t t',
-  (type_univ x t) --->α (type_univ y (type_subst x (type_var y) t))
+
+  (type_subst1 x (type_var y) t t') ->
+  (type_univ x t) --->α (type_univ y t')
 
   | TAlpha_SubUniv : forall x τ τ',
     (τ --->α τ') ->
-    [< ∀x,τ >] --->α [< ∀x,τ' >]
+    (type_univ x τ) --->α (type_univ x τ')
 
   | TAlpha_SubSpec1 : forall τ1 τ1' τ2,
     (τ1 --->α τ1') ->
-    [< <τ1 τ2> >] --->α [< <τ1' τ2> >]
+    (type_spec τ1 τ2) --->α (type_spec τ1' τ2)
 
   | TAlpha_SubSpec2 : forall τ1 τ2 τ2',
     (τ2 --->α τ2') ->
-    [< <τ1 τ2> >] --->α [< <τ1 τ2'> >]
+    (type_spec τ1 τ2) --->α (type_spec τ1 τ2')
 
   | TAlpha_SubFun1 : forall τ1 τ1' τ2,
     (τ1 --->α τ1') ->
-    [< τ1 -> τ2 >] --->α [< τ1' -> τ2 >]
+    (type_fun τ1 τ2) --->α (type_fun τ1' τ2)
 
   | TAlpha_SubFun2 : forall τ1 τ2 τ2',
     (τ2 --->α τ2') ->
-    [< τ1 -> τ2 >] --->α [< τ1 -> τ2' >]
+    (type_fun τ1 τ2) --->α (type_fun τ1 τ2')
 
   | TAlpha_SubMorph1 : forall τ1 τ1' τ2,
     (τ1 --->α τ1') ->
-    [< τ1 ->morph τ2 >] --->α [< τ1' ->morph τ2 >]
+    (type_morph τ1 τ2) --->α (type_morph τ1' τ2)
 
   | TAlpha_SubMorph2 : forall τ1 τ2 τ2',
     (τ2 --->α τ2') ->
-    [< τ1 ->morph τ2 >] --->α [< τ1 ->morph τ2' >]
+    (type_morph τ1 τ2) --->α (type_morph τ1 τ2')
 
   | TAlpha_SubLadder1 : forall τ1 τ1' τ2,
     (τ1 --->α τ1') ->
-    [< τ1 ~ τ2 >] --->α [< τ1' ~ τ2 >]
+    (type_ladder τ1 τ2) --->α (type_ladder τ1' τ2)
 
   | TAlpha_SubLadder2 : forall τ1 τ2 τ2',
     (τ2 --->α τ2') ->
-    [< τ1 ~ τ2 >] --->α [< τ1 ~ τ2' >]
+    (type_ladder τ1 τ2) --->α (type_ladder τ1 τ2')
 
 where "S '--->α' T" := (type_conv_alpha S T).
 
@@ -84,48 +86,38 @@ Lemma type_alpha_symm :
   forall σ τ,
   (σ --->α τ) -> (τ --->α σ).
 Proof.
-  intros.
+ (* TODO *)
-  induction H.
-  - admit.
-  - auto using TAlpha_Rename,type_subst,type_subst_symm, TAlpha_SubUniv.
-  - auto using TAlpha_SubSpec1.
-  - auto using TAlpha_SubSpec2.
-  - auto using TAlpha_SubFun1.
-  - auto using TAlpha_SubFun2.
-  - auto using TAlpha_SubMorph1.
-  - auto using TAlpha_SubMorph2.
-  - auto using TAlpha_SubLadder1.
-  - auto using TAlpha_SubLadder2.
 Admitted.
 
+
 (** Define all rewrite steps $\label{coq:type-dist}$ *)
 
 Reserved Notation "S '-->distribute-ladder' T" (at level 40).
 Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
   | L_DistributeOverSpec1 : forall x x' y,
-    [<  <x~x' y>  >]
+    (type_spec (type_ladder x x') y)
     -->distribute-ladder
-    [<  <x y>~<x' y>  >]
+    (type_ladder (type_spec x y) (type_spec x' y))
 
   | L_DistributeOverSpec2 : forall x y y',
-    [<  <x y~y'>  >]
+    (type_spec x (type_ladder y y'))
     -->distribute-ladder
-    [<  <x y>~<x y'>  >]
+    (type_ladder (type_spec x y) (type_spec x y'))
 
   | L_DistributeOverFun1 : forall x x' y,
-    [<  (x~x' -> y)  >]
+    (type_fun (type_ladder x x') y)
     -->distribute-ladder
-    [<  (x -> y) ~ (x' -> y)  >]
+    (type_ladder (type_fun x y) (type_fun x' y))
 
   | L_DistributeOverFun2 : forall x y y',
-    [<  (x -> y~y')  >]
+    (type_fun x (type_ladder y y'))
     -->distribute-ladder
-    [<  (x -> y) ~ (x -> y')  >]
+    (type_ladder (type_fun x y) (type_fun x y'))
 
   | L_DistributeOverMorph1 : forall x x' y,
-    [<  (x~x' ->morph y)  >]
+    (type_morph (type_ladder x x') y)
     -->distribute-ladder
-    [<  (x ->morph y) ~ (x' ->morph y)  >]
+    (type_ladder (type_morph x y) (type_morph x' y))
 
   | L_DistributeOverMorph2 : forall x y y',
     (type_morph x (type_ladder y y'))
@@ -139,34 +131,34 @@ where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
 Reserved Notation "S '-->condense-ladder' T" (at level 40).
 Inductive type_condense_ladder : type_term -> type_term -> Prop :=
   | L_CondenseOverSpec1 : forall x x' y,
-    [< <x y>~<x' y> >]
+    (type_ladder (type_spec x y) (type_spec x' y))
     -->condense-ladder
-    [< <x~x' y> >]
+    (type_spec (type_ladder x x') y)
 
   | L_CondenseOverSpec2 : forall x y y',
-    [< <x y>~<x y'> >]
+    (type_ladder (type_spec x y) (type_spec x y'))
     -->condense-ladder
-    [< <x y~y'> >]
+    (type_spec x (type_ladder y y'))
 
   | L_CondenseOverFun1 : forall x x' y,
-    [< (x -> y) ~ (x' -> y) >]
+    (type_ladder (type_fun x y) (type_fun x' y))
     -->condense-ladder
-    [< (x~x') -> y >]
+    (type_fun (type_ladder x x') y)
 
   | L_CondenseOverFun2 : forall x y y',
-    [< (x -> y) ~ (x -> y') >]
+    (type_ladder (type_fun x y) (type_fun x y'))
     -->condense-ladder
-    [< (x -> y~y') >]
+    (type_fun x (type_ladder y y'))
 
   | L_CondenseOverMorph1 : forall x x' y,
-    [< (x ->morph y) ~ (x' ->morph y) >]
+    (type_ladder (type_morph x y) (type_morph x' y))
     -->condense-ladder
-    [< (x~x' ->morph y) >]
+    (type_morph (type_ladder x x') y)
 
   | L_CondenseOverMorph2 : forall x y y',
-    [< (x ->morph y) ~ (x ->morph y') >]
+    (type_ladder (type_morph x y) (type_morph x y'))
     -->condense-ladder
-    [< (x ->morph y~y') >]
+    (type_morph x (type_ladder y y'))
 
 where "S '-->condense-ladder' T" := (type_condense_ladder S T).
 
@@ -220,25 +212,15 @@ Inductive type_eq : type_term -> type_term -> Prop :=
     y === z ->
     x === z
 
-  | TEq_SubFun : forall x x' y y',
-    x === x' ->
-    y === y' ->
-    [< x -> y >] === [< x' -> y' >]
-
-  | TEq_SubMorph : forall x x' y y',
-    x === x' ->
-    y === y' ->
-    [< x ->morph y >] === [< x' ->morph y' >]
-
   | TEq_LadderAssocLR : forall x y z,
-    [< (x~y)~z >]
+    (type_ladder (type_ladder x y) z)
     ===
-    [< x~(y~z) >]
+    (type_ladder x (type_ladder y z))
 
   | TEq_LadderAssocRL : forall x y z,
-    [< x~(y~z) >]
+    (type_ladder x (type_ladder y z))
     ===
-    [< (x~y)~z >]
+    (type_ladder (type_ladder x y) z)
 
   | TEq_Alpha : forall x y,
     x --->α y ->
@@ -269,11 +251,7 @@ Proof.
   apply TEq_Trans with (y:=y).
   apply IHtype_eq2.
   apply IHtype_eq1.
-
+  
-  apply TEq_SubFun.
-  auto. auto.
-  apply TEq_SubMorph.
-  auto. auto.
   apply TEq_LadderAssocRL.
   apply TEq_LadderAssocLR.
 
@@ -400,7 +378,7 @@ Admitted.
  *)
 
 Example example_flat_type :
-    type_is_flat [< <$"PosInt"$ $"10"$> >].
+    (type_is_flat (type_spec (type_id "PosInt") (type_id "10"))).
 Proof.
     apply FlatApp.
     apply FlatId.
@@ -408,15 +386,17 @@ Proof.
 Qed.
 
 Example example_lnf_type :
-    type_is_lnf [< [$"Char"$] ~ [$"Byte"$] >].
+    (type_is_lnf
+    (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
+               (type_spec (type_id "Seq") (type_id "Byte")))).
 Proof.
 Admitted.
 
 Example example_type_eq :
-    [< [$"Char"$ ~ $"Byte"$] >]
+    (type_spec (type_id "Seq") (type_ladder (type_id "Char") (type_id "Byte")))
     ===
-    [< [$"Char"$] ~ [$"Byte"$] >]
+    (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
-.
+               (type_spec (type_id "Seq") (type_id "Byte"))).
 Proof.
   apply TEq_Distribute.
   apply L_DistributeOverSpec2.

coq/morph.v

@@ -8,15 +8,13 @@ Require Import context.
 (* Given a context, there is a morphism path from τ to τ' *)
 Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
 
-Open Scope ladder_expr_scope.
-
 Inductive morphism_path : context -> type_term -> type_term -> Prop :=
   | M_Sub : forall Γ τ τ',
     (τ :<= τ') ->
     (Γ |- τ ~> τ')
 
   | M_Single : forall Γ h τ τ',
-    (context_contains Γ h [< τ ->morph τ' >]) ->
+    (context_contains Γ h (type_morph τ τ')) ->
     (Γ |- τ ~> τ')
 
   | M_Chain : forall Γ τ τ' τ'',
@@ -26,57 +24,58 @@ Inductive morphism_path : context -> type_term -> type_term -> Prop :=
 
   | M_Lift : forall Γ σ τ τ',
     (Γ |- τ ~> τ') ->
-    (Γ |- [< σ ~ τ >] ~> [< σ ~ τ' >])
+    (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))
 
   | M_MapSeq : forall Γ τ τ',
     (Γ |- τ ~> τ') ->
-    (Γ |- [< [τ] >] ~> [< [τ'] >])
+    (Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))
 
 where "Γ '|-' s '~>' t" := (morphism_path Γ s t).
 
-Lemma id_morphism_path : forall Γ τ, Γ |- τ ~> τ.
-Proof.
-  intros.
-  apply M_Sub, TSubRepr_Refl, TEq_Refl.
-Qed.
 
 Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
-  | Translate_Descend : forall Γ τ τ',
+  | Translate_Subtype : forall Γ τ τ',
     (τ :<= τ') ->
     (translate_morphism_path Γ τ τ'
-      (expr_morph "x" τ [{ %"x"% des τ' }]))
+        (expr_morph "x" τ (expr_var "x")))
 
   | Translate_Lift : forall Γ σ τ τ' m,
     (Γ |- τ ~> τ') ->
     (translate_morphism_path Γ τ τ' m) ->
-    (translate_morphism_path Γ [< σ ~ τ >] [< σ ~ τ' >]
+    (translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
-      (expr_morph "x" [< σ ~ τ >] [{ (m (%"x"% des τ)) as σ }]))
+        (expr_morph "x" (type_ladder σ τ)
+          (expr_ascend σ (expr_app m (expr_descend τ (expr_var "x"))))))
 
   | Translate_Single : forall Γ h τ τ',
-    (context_contains Γ h [< τ ->morph τ' >]) ->
+    (context_contains Γ h (type_morph τ τ')) ->
-    (translate_morphism_path Γ τ τ' [{ %h% }])
+    (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" τ [{ m2 (m1 %"x"%) }]))
+      (expr_morph "x" τ (expr_app m2 (expr_app m1 (expr_var "x")))))
 
   | Translate_MapSeq : forall Γ τ τ' m,
     (translate_morphism_path Γ τ τ' m) ->
-    (translate_morphism_path Γ [< [τ] >] [< [τ'] >]
+    (translate_morphism_path Γ
-      [{
+      (type_spec (type_id "Seq") τ)
-        λ"xs",[τ] ↦morph (%"map"% # τ # τ' m %"xs"%)
+      (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))
 
-  |- [< [ $"Hue"$~$"Angle"$~$"Degrees"$~$"ℝ"$ ] >]
+  |- [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Degrees"$~$"ℝ"$> >]
-  ~> [< [ $"Hue"$~$"Angle"$~$"Radians"$~$"ℝ"$ ] >]
+  ~> [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Radians"$~$"ℝ"$> >]
 .
 Proof.
   intros.

coq/smallstep.v

@@ -16,19 +16,19 @@ Inductive expr_alpha : expr_term -> expr_term -> Prop :=
 
   | EAlpha_SubAbs : forall x τ e e',
     (e -->α e') ->
-    [{ λ x , τ ↦ e }] -->α [{ λ x , τ ↦ e' }]
+    (expr_abs x τ e) -->α (expr_abs x τ e')
 
   | EAlpha_SubTyAbs : forall α e e',
     (e -->α e') ->
-    [{ Λ α ↦ e }] -->α [{ Λ α ↦ e' }]
+    (expr_ty_abs α e) -->α (expr_ty_abs α e')
 
   | EAlpha_SubApp1 : forall e1 e1' e2,
     (e1 -->α e1') ->
-    [{ e1 e2 }] -->α [{ e1' e2 }]
+    (expr_app e1 e2) -->α (expr_app e1' e2)
 
   | EAlpha_SubApp2 : forall e1 e2 e2',
     (e2 -->α e2') ->
-    [{ e1 e2 }] -->α [{ e1 e2' }]
+    (expr_app e1 e2) -->α (expr_app e1 e2')
 
 where "s '-->α' t" := (expr_alpha s t).
 
@@ -45,45 +45,45 @@ Qed.
 Inductive beta_step : expr_term -> expr_term -> Prop :=
   | E_App1 : forall e1 e1' e2,
     e1 -->β e1' ->
-    [{ e1 e2 }] -->β [{ e1' e2 }]
+    (expr_app e1 e2) -->β (expr_app e1' e2)
 
   | E_App2 : forall v1 e2 e2',
     (is_value v1) ->
     e2 -->β e2' ->
-    [{ v1 e2 }] -->β [{ v1 e2' }]
+    (expr_app v1 e2) -->β (expr_app v1 e2')
 
   | E_TypApp : forall e e' τ,
     e -->β e' ->
-    [{ Λ τ ↦ e }] -->β [{ Λ τ ↦ e' }]
+    (expr_ty_app e τ) -->β (expr_ty_app e' τ)
 
   | E_TypAppLam : forall α e τ,
-    [{ (Λ α ↦ e) # τ }] -->β (expr_specialize α τ e)
+    (expr_ty_app (expr_ty_abs α e) τ) -->β (expr_specialize α τ e)
 
   | E_AppLam : forall x τ e a,
-    [{ (λ x , τ ↦ e) a }] -->β (expr_subst x a e)
+    (expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
 
   | E_AppMorph : forall x τ e a,
-    [{ (λ x , τ ↦morph e) a }] -->β (expr_subst x a e)
+    (expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
 
   | E_Let : forall x e a,
-    [{ let x := a in e }] -->β (expr_subst x a e)
+    (expr_let x a e) -->β (expr_subst x a e)
 
   | E_StripAscend : forall τ e,
-    [{ e as τ }] -->β e
+    (expr_ascend τ e) -->β e
 
   | E_StripDescend : forall τ e,
-    [{ e des τ }] -->β e
+    (expr_descend τ e) -->β e
 
   | E_Ascend : forall τ e e',
     (e -->β e') ->
-    [{ e as τ }] -->β [{ e' as τ }]
+    (expr_ascend τ e) -->β (expr_ascend τ e')
 
   | E_AscendCollapse : forall τ' τ e,
-    [{ (e as τ) as τ' }] -->β [{ e as (τ'~τ) }]
+    (expr_ascend τ' (expr_ascend τ e)) -->β (expr_ascend (type_ladder τ' τ) e)
 
   | E_DescendCollapse : forall τ' τ e,
     (τ':<=τ) ->
-    [{ (e des τ') des τ }] -->β [{ e des τ }]
+    (expr_descend τ (expr_descend τ' e)) -->β (expr_descend τ e)
 
 where "s '-->β' t" := (beta_step s t).
 
@@ -102,7 +102,7 @@ Notation " s -->β* t " := (multi beta_step s t) (at level 40).
 Example reduce1 :
   [{
     let "deg2turns" :=
-       (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
+       (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
                 ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$))
     in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
   }]
@@ -111,7 +111,7 @@ Example reduce1 :
      ((%"/"% %"60"%) %"360"%) as $"Angle"$~$"Turns"$
   }].
 Proof.
-  apply Multi_Step with (y:=[{ (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
+  apply Multi_Step with (y:=[{ (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
                 ↦morph (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$)) (%"60"% as $"Angle"$~$"Degrees"$) }]).
   apply E_Let.
 

coq/soundness.v

@@ -8,6 +8,7 @@ Require Import morph.
 Require Import smallstep.
 Require Import typing.
 
+
 Lemma typing_weakening : forall Γ e τ x σ,
   (Γ |- e \is τ) ->
   ((ctx_assign x σ Γ) |- e \is τ)
@@ -16,22 +17,17 @@ Proof.
   intros.
   induction H.
 
-  - apply T_Var.
+  apply T_Var.
-    apply C_shuffle.
+  apply C_shuffle.
-    apply H.
+  apply H.
   
-  - apply T_Let with (σ:=σ0).
+  apply T_Let with (σ:=σ0).
-    apply IHexpr_type1.
+  apply IHexpr_type1.
-    
+  admit.
-    admit.
+
-Admitted.
-Lemma map_type : forall Γ,
-  Γ |- [{ %"map"% }] \is [<
-       ∀"σ",∀"τ", (%"σ"% -> %"τ"%) -> [%"σ"%] -> [%"τ"%]
-  >].
-Proof.
 Admitted.
 
+
 Lemma morphism_path_solves_type : forall Γ τ τ' m,
   (translate_morphism_path Γ τ τ' m) ->
   Γ |- m \is (type_morph τ τ')
@@ -42,7 +38,7 @@ Proof.
 
   (* Sub *)
   apply T_MorphAbs.
-  apply T_Descend with (τ:=τ).
+  apply T_DescendImplicit with (τ:=τ).
   apply T_Var.
   apply C_take.
   apply H.
@@ -58,7 +54,7 @@ Proof.
   apply T_Var.
   apply C_take.
   apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
-  apply id_morphism_path.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
 
   (* Single *)
   apply T_Var.
@@ -70,7 +66,7 @@ Proof.
   apply T_MorphFun.
   apply typing_weakening.
   apply IHtranslate_morphism_path2.
-
+  
   apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
   apply T_MorphFun.
   apply typing_weakening.
@@ -78,30 +74,15 @@ Proof.
 
   apply T_Var.
   apply C_take.
-  apply id_morphism_path.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
-  apply id_morphism_path.
+  apply M_Sub, TSubRepr_Refl, TEq_Refl.
 
   (* Map Sequence *)
   apply T_MorphAbs.
   apply T_App with (σ':=(type_spec (type_id "Seq") τ)) (σ:=(type_spec (type_id "Seq") τ)).
   apply T_App with (σ':=(type_fun τ τ')) (σ:=(type_fun τ τ')).
 
-  set (k:=[< (%"σ"% -> %"τ"%) -> <$"Seq"$ %"σ"%> -> <$"Seq"$ %"τ"%> >]).
-  set (k1:=[< (τ -> %"τ"%) -> <$"Seq"$ τ> -> <$"Seq"$ %"τ"%> >]).
-  set (k2:=[< (τ -> τ') -> <$"Seq"$ τ> -> <$"Seq"$ τ'> >]).
-
-  set (P:=(type_subst "τ" τ' k1) = k2).
-  
-(*  apply T_TypeApp with (α:="τ"%string) (τ:=k2).*)
-(*  apply T_TypeApp with (α:="τ"%string) (τ:=(type_subst "τ" τ' k1)).*)
-(*
-  apply map_type.
-
-  apply TSubst_UnivReplace.
   admit.
-  admit.
-
-  apply TSubst_UnivReplace.
 
   apply T_MorphFun.
   apply typing_weakening.
@@ -111,7 +92,6 @@ Proof.
   apply T_Var.
   apply C_take.
   apply M_Sub, TSubRepr_Refl, TEq_Refl.
-  *)
 Admitted.
 
 (* reduction step preserves well-typedness *)
@@ -206,7 +186,7 @@ Proof.
     apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ').
     apply T_MorphFun.
     apply T_MorphAbs.
-    apply T_Descend with (τ:=τ0).
+    apply T_DescendImplicit with (τ:=τ0).
     apply T_Var.
     apply C_take.
     apply H3.
@@ -324,7 +304,7 @@ Proof.
   apply H0.
 
   (* e is Desecension *)
-  apply T_Descend with (τ:=τ).
+  apply T_DescendImplicit with (τ:=τ).
   apply IHtranslate_typing.
   apply H0.
   apply H1.

coq/subst.v

@@ -1,34 +1,60 @@
-From Coq Require Import Strings.String.
+ From Coq Require Import Strings.String.
-From Coq Require Import Lists.List.
-Import ListNotations.
 Require Import terms.
 
+(* 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 τ))
+.
 
-Fixpoint type_fv (τ : type_term) {struct τ} : (list string) :=
-  match τ with
-  | type_id s => []
-  | type_var α => [α]
-  | type_univ α τ => (remove string_dec α (type_fv τ))
-  | type_spec σ τ => (type_fv σ) ++ (type_fv τ)
-  | type_fun σ τ => (type_fv σ) ++ (type_fv τ)
-  | type_morph σ τ => (type_fv σ) ++ (type_fv τ)
-  | type_ladder σ τ => (type_fv σ) ++ (type_fv τ)
-  end.
 
 Open Scope ladder_type_scope.
-Example ex_type_fv1 :
+Example ex_type_free_var1 :
-  (In "T"%string (type_fv [< ∀"U",%"T"% >]))
+  (type_var_free "T" (type_univ "U" (type_var "T")))
 .
-Proof. simpl. left. auto. Qed.
+Proof.
+  apply TFree_Univ.
+  easy.
+  apply TFree_Var.
+Qed.
 
 Open Scope ladder_type_scope.
-Example ex_type_fv2 :
+Example ex_type_free_var2 :
-  ~(In "T"%string (type_fv [< ∀"T",%"T"% >]))
+  ~(type_var_free "T" (type_univ "T" (type_var "T")))
 .
-Proof. simpl. auto. Qed.
+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) : type_term :=
+Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
   match t0 with
   | type_var name => if (eqb v name) then n else t0
   | type_fun t1 t2 => (type_fun (type_subst v n t1) (type_subst v n t2))
@@ -38,14 +64,12 @@ Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) : 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) ->
+    ~(x = y) ->
     (type_subst1 x σ (type_var y) (type_var y))
 
   | TSubst_UnivReplace : forall y τ τ',
@@ -77,56 +101,6 @@ Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop
     (type_subst1 x σ τ2 τ2') ->
     (type_subst1 x σ (type_ladder τ1 τ2) (type_ladder τ1' τ2'))
 .
-*)
-
-Lemma type_subst_symm :
-  forall x y τ τ',
-  ((type_subst x (type_var y) τ) = τ') ->
-  ((type_subst y (type_var x) τ') = τ)
-.
-Proof.
-  intros.
-  induction H.
-
-  unfold type_subst.
-  induction τ.
-  reflexivity.
-
-  
-Admitted.
-
-Lemma type_subst_fresh :
-  forall α τ u,
-  ~ (In α (type_fv τ))
-  -> (type_subst α u τ) = τ
-.
-Proof.
-  intros.
-  unfold type_subst.
-  induction τ.
-  reflexivity.
-
-  
-  unfold eqb.
-
-  admit.
-(*
-  apply TSubst_Id.
-  apply TSubst_VarKeep.
-  contradict H.
-  rewrite H.
-  apply TFree_Var.
-
-  apply TSubst_Fun.
-  apply IHτ1.
-
-  contradict H.
-  apply TFree_Fun.
-  apply H.
-  apply 
-  *)
-Admitted.
-
 
 (* scoped variable substitution, replaces free occurences of v with n in expression e *)
 Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=

coq/terms.v

@@ -64,66 +64,58 @@ Declare Custom Entry ladder_type.
 Declare Custom Entry ladder_expr.
 
 Notation "[< t >]" := t
-  (t custom ladder_type at level 99) : ladder_type_scope.
+  (t custom ladder_type at level 80) : ladder_type_scope.
 Notation "t" := t
   (in custom ladder_type at level 0, t ident) : 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).
 Notation "'<' σ τ '>'" := (type_spec σ τ)
   (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
-Notation "'[' τ ']'" := (type_spec (type_id "Seq") τ)
-  (in custom ladder_type at level 70) : ladder_type_scope.
 Notation "'(' τ ')'" := τ
-  (in custom ladder_type at level 5) : ladder_type_scope.
+  (in custom ladder_type at level 70) : ladder_type_scope.
 Notation "σ '->' τ" := (type_fun σ τ)
   (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
 Notation "σ '->morph' τ" := (type_morph σ τ)
   (in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
 Notation "σ '~' τ" := (type_ladder σ τ)
-  (in custom ladder_type at level 20, right associativity) : ladder_type_scope.
+  (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
 Notation "'$' x '$'" := (type_id x%string)
-  (in custom ladder_type at level 10, x constr) : ladder_type_scope.
+  (in custom ladder_type at level 0, x constr) : ladder_type_scope.
 Notation "'%' x '%'" := (type_var x%string)
-  (in custom ladder_type at level 10, x constr) : ladder_type_scope.
+  (in custom ladder_type at level 0, x constr) : ladder_type_scope.
 
 Notation "[{ e }]" := e
-  (e custom ladder_expr at level 99) : ladder_expr_scope.
+  (e custom ladder_expr at level 80) : ladder_expr_scope.
 Notation "e" := e
   (in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
 Notation "'%' x '%'" := (expr_var x%string)
-  (in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
+  (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
 Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
-  (in custom ladder_expr at level 10, t constr, e custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
+  (in custom ladder_expr at level 10, t constr, e custom ladder_expr at level 80) : ladder_expr_scope.
-Notation "'λ' x ',' τ '↦' e" := (expr_abs x τ e)
+Notation "'λ' x τ '↦' e" := (expr_abs x τ e)
-  (in custom ladder_expr at level 70, x constr, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
+  (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)
+Notation "'λ' x τ '↦morph' e" := (expr_morph x τ e)
-  (in custom ladder_expr at level 70, x constr, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
+  (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 60, x constr, e custom ladder_expr at level 80, t custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
+  (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 "e 'des' τ" := (expr_descend τ 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 90, e2 custom ladder_expr at next level) : ladder_expr_scope.
+  (in custom ladder_expr at level 50) : ladder_expr_scope.
-Notation "e '#' τ" := (expr_ty_app e τ)
-  (in custom ladder_expr at level 80, τ custom ladder_type at level 101, left associativity) : ladder_expr_scope.
 Notation "'(' e ')'" := e
-  (in custom ladder_expr, e custom ladder_expr at next level, left associativity) : ladder_expr_scope.
+  (in custom ladder_expr at level 0) : ladder_expr_scope.
-
-
-Print Grammar constr.
 
 (* EXAMPLES *)
 
 Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
 
-Check [< ∀"α", [%"α"%] ~ <$"List"$ %"α"%> >].
+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"% }].
-Definition polymorphic_identity2 : expr_term := [{ Λ"T" ↦ λ"y",%"T"% ↦ %"y"% }].
 
 Compute polymorphic_identity1.
 

coq/terms_debruijn.v

@@ -1,281 +0,0 @@
-From Coq Require Import Strings.String.
-From Coq Require Import Lists.List.
-Import ListNotations.
-
-Require Import terms.
-
-Inductive type_DeBruijn : Type :=
-  | ty_id : string -> type_DeBruijn
-  | ty_fvar : string -> type_DeBruijn
-  | ty_bvar : nat -> type_DeBruijn
-  | ty_univ : type_DeBruijn -> type_DeBruijn
-  | ty_spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | ty_func  : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | ty_morph : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-  | ty_ladder : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
-.
-
-Inductive expr_DeBruijn : Type :=
-  | ex_var : nat -> expr_DeBruijn
-  | ex_ty_abs : expr_DeBruijn -> expr_DeBruijn
-  | ex_ty_app : expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn
-  | ex_abs   : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | ex_morph : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | ex_app : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | varlet : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | ex_ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | ex_descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-.
-
-(* get the list of all free variables in a type term *)
-Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : (list string) :=
-  match τ with
-  | ty_id s => []
-  | ty_fvar α => [α]
-  | ty_bvar x => []
-  | ty_univ τ => (type_fv τ)
-  | ty_spec σ τ => (type_fv σ) ++ (type_fv τ)
-  | ty_func σ τ => (type_fv σ) ++ (type_fv τ)
-  | ty_morph σ τ => (type_fv σ) ++ (type_fv τ)
-  | ty_ladder σ τ => (type_fv σ) ++ (type_fv τ)
-  end.
-
-(* substitute free variable x with type σ in τ *)
-Fixpoint subst_type (x:string) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
-  match τ with
-  | ty_id s => ty_id s
-  | ty_fvar s => if eqb x s then σ else τ
-  | ty_bvar y => ty_bvar y
-  | ty_univ τ => ty_univ (subst_type x σ τ)
-  | ty_spec τ1 τ2 => ty_spec (subst_type x σ τ1) (subst_type x σ τ2)
-  | ty_func τ1 τ2 => ty_func (subst_type x σ τ1) (subst_type x σ τ2)
-  | ty_morph τ1 τ2 => ty_morph (subst_type x σ τ1) (subst_type x σ τ2)
-  | ty_ladder τ1 τ2 => ty_ladder (subst_type x σ τ1) (subst_type x σ τ2)
-  end.
-
-(* replace a free variable with a new (dangling) bound variable *)
-Fixpoint type_bind_fvar (x:string) (n:nat) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
-  match τ with
-  | ty_id s => ty_id s
-  | ty_fvar s => if eqb x s then ty_bvar n else τ
-  | ty_bvar n => ty_bvar n
-  | ty_univ τ1 => ty_univ (type_bind_fvar x (S n) τ1)
-  | ty_spec τ1 τ2 => ty_spec (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
-  | ty_func τ1 τ2 => ty_func (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
-  | ty_morph τ1 τ2 => ty_morph (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
-  | ty_ladder τ1 τ2 => ty_ladder (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
-  end.
-
-(* replace (dangling) index with another type *)
-Fixpoint type_open_rec (k:nat) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
-  match τ with
-    | ty_id s => ty_id s
-    | ty_fvar s => ty_fvar s
-    | ty_bvar i => if Nat.eqb k i then σ else τ
-    | ty_univ τ1 => ty_univ (type_open_rec (S k) σ τ1)
-    | ty_spec τ1 τ2 => ty_spec (type_open_rec k σ τ1) (type_open_rec k σ τ2)
-    | ty_func τ1 τ2 => ty_func (type_open_rec k σ τ1) (type_open_rec k σ τ2)
-    | ty_morph τ1 τ2 => ty_morph (type_open_rec k σ τ1) (type_open_rec k σ τ2)
-    | ty_ladder τ1 τ2 => ty_ladder (type_open_rec k σ τ1) (type_open_rec k σ τ2)
-  end.
-
-Notation "'[' z '~>' u ']' e" := (subst_type z u e) (at level 68).
-Notation "'{' k '~>' σ '}' τ" := (type_open_rec k σ τ) (at level 67).
-Definition type_open σ τ := type_open_rec 0 σ τ.
-
-(* is the type locally closed ? *)
-Inductive type_lc : type_DeBruijn -> Prop :=
-  | Tlc_Id : forall s, type_lc (ty_id s)
-  | Tlc_Var : forall s, type_lc (ty_fvar s)
-  | Tlc_Univ : forall τ1 L,
-      (forall x, ~ (In x L) -> type_lc (type_open (ty_fvar x) τ1)) ->
-      type_lc (ty_univ τ1)
-  | Tlc_Spec : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_spec τ1 τ2)
-  | Tlc_Func : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_func τ1 τ2)
-  | Tlc_Morph : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_morph τ1 τ2)
-  | Tlc_Ladder : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_ladder τ1 τ2)
-.
-
-(* number of abstractions *)
-Fixpoint type_debruijn_depth (τ:type_DeBruijn) : nat :=
-  match τ with
-  | ty_id s => 0
-  | ty_fvar s => 0
-  | ty_bvar x => 0
-  | ty_func s t => max (type_debruijn_depth s) (type_debruijn_depth t)
-  | ty_morph s t => max (type_debruijn_depth s) (type_debruijn_depth t)
-  | ty_univ t => (1 + (type_debruijn_depth t))
-  | ty_spec s t => ((type_debruijn_depth s) - 1)
-  | ty_ladder s t => max (type_debruijn_depth s) (type_debruijn_depth t)
-  end.
-
-Fixpoint type_named2debruijn (τ:type_term) {struct τ} : type_DeBruijn :=
-  match τ with
-  | type_id s => ty_id s
-  | type_var s => ty_fvar s
-  | type_univ x t => let t':=(type_named2debruijn t) in (ty_univ (type_bind_fvar x 0 t'))
-  | type_spec s t => ty_spec (type_named2debruijn s) (type_named2debruijn t)
-  | type_fun s t => ty_func (type_named2debruijn s) (type_named2debruijn t)
-  | type_morph s t => ty_morph (type_named2debruijn s) (type_named2debruijn t)
-  | type_ladder s t => ty_ladder (type_named2debruijn s) (type_named2debruijn t)
-  end.
-
-Coercion type_named2debruijn : type_term >-> type_DeBruijn.
-
-Lemma list_in_tail : forall x (E:list string) f,
-  In x E ->
-  In x (cons f E).
-Proof.
-  intros.
-  simpl.
-  right.
-  apply H.
-Qed.
-
-Lemma list_in_concatA : forall x (E:list string) (F:list string),
-  In x E ->
-  In x (E ++ F).
-Proof.
-Admitted.
-
-Lemma list_in_concatB : forall x (E:list string) (F:list string),
-  In x F ->
-  In x (E ++ F).
-Proof.
-  intros.
-  induction E.
-  auto.
-  apply list_in_tail.
-  
-Admitted.
-
-Lemma list_notin_singleton : forall (x:string) (y:string),
-  ((eqb x y) = false) -> ~ In x [ y ].
-Proof.
-Admitted.
-
-Lemma list_elim_notin_singleton : forall (x:string) (y:string),
-  ~ In x [y] -> ((eqb x y) = false).
-Proof.
-Admitted.
-
-
-Lemma subst_fresh_type : forall (x : string) (τ:type_DeBruijn) (σ:type_DeBruijn),
-  ~(In x (type_fv τ)) ->
-  (subst_type x σ τ) = τ
-.
-Proof.
-  intros.
-  induction τ.
-
-  - reflexivity.
-
-  - unfold type_fv in H.
-    apply list_elim_notin_singleton in H.
-    simpl.
-    case_eq (x =? s)%string.
-    congruence.
-    reflexivity.
-
-  - reflexivity.
-
-  - simpl. rewrite IHτ.
-    reflexivity.
-    apply H.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    simpl type_fv in H.
-    contradict H. apply list_in_concatB, H.
-    contradict H. apply list_in_concatA, H.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    contradict H. apply list_in_concatB, H.
-    contradict H. apply list_in_concatA, H.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    contradict H. apply list_in_concatB, H.
-    contradict H. apply list_in_concatA, H.
-
-  - simpl. rewrite IHτ1, IHτ2.
-    reflexivity.
-    contradict H. apply list_in_concatB, H.
-    contradict H. apply list_in_concatA, H.
-Qed.
-
-
-
-Lemma open_rec_lc_core : forall τ j σ1 i σ2,
-  i <> j ->
-  {j ~> σ1} τ = {i ~> σ2} ({j ~> σ1} τ) ->
-  τ = {i ~> σ1} τ.
-
-Proof with (eauto with *).
-  induction τ;
-  intros j v i u Neq H;
-  simpl in *; try solve [inversion H; f_equal; eauto].
-
-(*  case (ty_bvar).*)
-    destruct (Nat.eqb j n)...
-    destruct (Nat.eqb i n)...
-  
-Admitted.
-
-
-Lemma type_open_rec_lc : forall k σ τ,
-  type_lc τ ->
-  { k ~> σ } τ = τ.
-Proof.
-  intros.
-  generalize dependent k.
-  induction H.
-  - auto.
-  - auto.
-  - intro k.
-    unfold type_open in *.
-    (*
-    pick fresh x for L.
-    apply open_rec_lc_core with (i := S k) (j := 0) (u := u) (v := x). auto. auto.
-    *)
-    admit.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-Admitted.
-
-Lemma type_subst_open_rec : forall τ1 τ2 σ x k,
-  type_lc σ ->
-  [x ~> σ] ({k ~> τ2} τ1) = {k ~> [x ~> σ] τ2} ([x ~> σ] τ1).
-Proof.
-  intros.
-  induction τ1.
-
-  (* id *)
-  - auto.
-
-  (* free var *)
-  - simpl.
-    case_eq (eqb x s).
-    intro.
-    apply eq_sym.
-    apply type_open_rec_lc, H.
-    auto.
-
-  (* bound var *)
-  - simpl.
-    case_eq (Nat.eqb k n).
-    auto.
-    auto.
-
-  (* univ *)
-  - simpl.
-    admit.
-
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
-Admitted.

coq/typing.v

@@ -11,42 +11,40 @@ Require Import morph.
 
 (** Typing Derivation *)
 
-Open Scope ladder_type_scope.
-Open Scope ladder_expr_scope.
-
 Reserved Notation "Gamma '|-' x '\is' 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 τ ->
+    (context_contains Γ x τ) ->
-    Γ |- [{ %x% }] \is τ
+    (Γ |- (expr_var x) \is τ)
 
   | T_Let : forall Γ s σ t τ x,
-    Γ |- s \is σ ->
+    (Γ |- s \is σ) ->
-    (ctx_assign x σ Γ) |- t \is τ ->
+    ((ctx_assign x σ Γ) |- t \is τ) ->
-    Γ |- [{ let x := s in t }] \is τ
+    (Γ |- (expr_let x s t) \is τ)
 
   | T_TypeAbs : forall Γ e τ α,
     Γ |- e \is τ ->
-    Γ |- [{ Λ α ↦ e }] \is [< ∀α,τ >]
+    Γ |- (expr_ty_abs α e) \is (type_univ α τ)
 
-  | T_TypeApp : forall Γ α e σ τ,
+  | T_TypeApp : forall Γ α e σ τ τ',
-    Γ |- e \is [< ∀α, τ >] ->
+    Γ |- e \is (type_univ α τ) ->
-    Γ |- [{ e # σ }] \is (type_subst α σ τ)
+    (type_subst1 α σ τ τ') ->
+    Γ |- (expr_ty_app e σ) \is τ'
 
   | T_Abs : forall Γ x σ t τ,
-    (ctx_assign x σ Γ) |- t \is τ ->
+    ((ctx_assign x σ Γ) |- t \is τ) ->
-    Γ |- [{ λ x , σ ↦ t }] \is [< σ -> τ >]
+    (Γ |- (expr_abs x σ t) \is (type_fun σ τ))
 
-  | T_MorphAbs : forall Γ x σ t τ,
+  | T_MorphAbs : forall Γ x σ e τ,
-    (ctx_assign x σ Γ) |- t \is τ ->
+    ((ctx_assign x σ Γ) |- e \is τ) ->
-    Γ |- [{ λ x , σ ↦morph t }] \is [< σ ->morph τ >]
+    Γ |- (expr_morph x σ e) \is (type_morph σ τ)
 
   | T_App : forall Γ f a σ' σ τ,
-    (Γ |- f \is [< σ -> τ >]) ->
+    (Γ |- f \is (type_fun σ τ)) ->
     (Γ |- a \is σ') ->
     (Γ |- σ' ~> σ) ->
-    (Γ |- [{ (f a) }] \is τ)
+    (Γ |- (expr_app f a) \is τ)
 
   | T_MorphFun : forall Γ f σ τ,
     Γ |- f \is (type_morph σ τ) ->
@@ -54,7 +52,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
 
   | T_Ascend : forall Γ e τ τ',
     (Γ |- e \is τ) ->
-    (Γ |- [{ e as τ' }] \is [< τ' ~ τ >])
+    (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ))
 
   | T_DescendImplicit : forall Γ x τ τ',
     Γ |- x \is τ ->
@@ -64,7 +62,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
   | T_Descend : forall Γ x τ τ',
     Γ |- x \is τ ->
     (τ :<= τ') ->
-    Γ |- [{ x des τ' }] \is τ'
+    Γ |- (expr_descend τ' x) \is τ'
 
 where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
@@ -77,85 +75,73 @@ Definition is_well_typed (e:expr_term) : Prop :=
 Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
   | Expand_Var : forall Γ x τ,
     (Γ |- (expr_var x) \is τ) ->
-    (translate_typing Γ [{ %x% }] τ [{ %x% }])
+    (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 Γ
+    (translate_typing Γ (expr_let x e t) τ (expr_let x e' t'))
-      [{ let x := e in t }]
-      τ
-      [{ let x := e' in t' }])
 
   | Expand_TypeAbs : forall Γ α e e' τ,
     (Γ |- e \is τ) ->
     (translate_typing Γ e τ e') ->
     (translate_typing Γ
-      [{ Λ α ↦ e }]
+      (expr_ty_abs α e)
-      [< ∀ α,τ >]
+      (type_univ α τ)
-      [{ Λ α ↦ e' }])
+      (expr_ty_abs α e'))
 
   | Expand_TypeApp : forall Γ e e' σ α τ,
     (Γ |- e \is (type_univ α τ)) ->
     (translate_typing Γ e τ e') ->
-    (translate_typing Γ
+    (translate_typing Γ (expr_ty_app e τ) (type_subst α σ τ) (expr_ty_app e' τ))
-      [{ e # τ }]
-      (type_subst α σ τ)
-      [{ 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 Γ
+    (translate_typing Γ (expr_abs x σ e) (type_fun σ τ) (expr_abs x σ e'))
-      [{ λ x , σ ↦ e }]
-      [< σ -> τ >]
-      [{ λ 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 Γ
+    (translate_typing Γ (expr_morph x σ e) (type_morph σ τ) (expr_morph x σ e'))
-      [{ λ x , σ ↦morph e }]
-      [< σ ->morph τ >]
-      [{ λ x , σ ↦morph e' }])
 
   | Expand_App : forall Γ f f' a a' m σ τ σ',
     (Γ |- f \is (type_fun σ τ)) ->
     (Γ |- a \is σ') ->
     (Γ |- σ' ~> σ) ->
-    (translate_typing Γ f [< σ -> τ >] f') ->
+    (translate_typing Γ f (type_fun σ τ) f') ->
     (translate_typing Γ a σ' a') ->
     (translate_morphism_path Γ σ' σ m) ->
-    (translate_typing Γ [{ f a }] τ [{ f' (m a') }])
+    (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 [< σ ->morph τ >] f') ->
+    (translate_typing Γ f (type_morph σ τ) f') ->
-    (translate_typing Γ f [< σ -> τ >] f')
+    (translate_typing Γ f (type_fun σ τ) f')
 
   | Expand_Ascend : forall Γ e e' τ τ',
     (Γ |- e \is τ) ->
-    (Γ |- [{ e as τ' }] \is [< τ' ~ τ >]) ->
+    (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ)) ->
     (translate_typing Γ e τ e') ->
-    (translate_typing Γ [{ e as τ' }] [< τ' ~ τ >] [{ e' as τ' }])
+    (translate_typing Γ (expr_ascend τ' e) (type_ladder τ' τ) (expr_ascend τ' e'))
 
   | Expand_Descend : forall Γ e e' τ τ',
     (Γ |- e \is τ) ->
     (τ :<= τ') ->
-    (Γ |- [{ e des τ' }] \is τ') ->
+    (Γ |- e \is τ') ->
     (translate_typing Γ e τ e') ->
-    (translate_typing Γ e τ' [{ e' des τ' }])
+    (translate_typing Γ e τ' e')
 .
 
 (* Examples *)
 
 Example typing1 :
-  ctx_empty |- [{ Λ"T" ↦ λ "x",%"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
+  ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
 Proof.
   intros.
   apply T_TypeAbs.
@@ -165,7 +151,7 @@ Proof.
 Qed.
 
 Example typing2 :
-  ctx_empty |- [{ Λ"T" ↦ λ "x",%"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
+  ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
 Proof.
   intros.
   apply T_DescendImplicit with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
@@ -177,11 +163,14 @@ Proof.
   apply TSubRepr_Refl.
   apply TEq_Alpha.
   apply TAlpha_Rename.
+  apply TSubst_Fun.
+  apply TSubst_VarReplace.
+  apply TSubst_VarReplace.
 Qed.
 
 Example typing3 :
   ctx_empty |- [{
-    Λ"T" ↦ Λ"U" ↦ λ"x",%"T"% ↦ λ"y",%"U"% ↦ %"y"%
+    Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"y"%
   }] \is [<
        ∀"S",∀"T",(%"S"%->%"T"%->%"T"%)
   >].
@@ -197,14 +186,26 @@ Proof.
   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.
 
 Example typing4 : (is_well_typed
-  [{ Λ"T" ↦ Λ"U" ↦ λ"x",%"T"% ↦ λ"y",%"U"% ↦ %"x"% }]
+  [{ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% }]
 ).
 Proof.
   unfold is_well_typed.
@@ -217,6 +218,8 @@ Proof.
   apply C_shuffle, C_take.
 Qed.
 
+Open Scope ladder_expr_scope.
+
 Example typing5 :
   (ctx_assign "60" [< $"ℝ"$ >]
   (ctx_assign "360" [< $"ℝ"$ >]
@@ -225,7 +228,7 @@ Example typing5 :
   |-
   [{
     let "deg2turns" :=
-       (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
+       (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
                 ↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$))
     in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
   }]
@@ -268,116 +271,4 @@ Proof.
   apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
 Qed.
 
-
+End Typing.
-Ltac var_typing := auto using T_Var, C_shuffle, C_take.
-Ltac repr_subtype := auto using TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl, TEq_LadderAssocLR.
-
-Example expand1 :
-  (translate_typing
-      (ctx_assign "60" [< $"ℝ"$ >]
-      (ctx_assign "360" [< $"ℝ"$ >]
-      (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
-        ctx_empty)))
-  [{
-    let "deg2turns" :=
-       (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
-                ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$)) in
-    let "sin" := (λ"α",$"Angle"$~$"Turns"$~$"ℝ"$ ↦ (%"α"% des $"ℝ"$)) in
-    ( %"sin"% (%"60"% as $"Angle"$~$"Degrees"$) )
-  }]
-  [<
-     $"ℝ"$
-  >]
-  [{
-    let "deg2turns" :=
-       (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
-                ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$)) in
-    let "sin" := (λ"α",$"Angle"$~$"Turns"$~$"ℝ"$ ↦ (%"α"% des $"ℝ"$)) in
-    (%"sin"% (%"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$)))
-  }])
-.
-Proof.
-  apply Expand_Let with (σ:=[< ($"Angle"$~$"Degrees"$)~$"ℝ"$ ->morph ($"Angle"$~$"Turns"$)~$"ℝ"$ >]).
-
-  - apply T_DescendImplicit with (τ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$ ~ $"ℝ"$ >]).
-    2: {
-      apply TSubRepr_Refl.
-      apply TEq_SubMorph.
-      apply TEq_LadderAssocRL.
-      apply TEq_LadderAssocRL.
-    }
-    apply T_MorphAbs.
-    apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]).
-    2: {
-      apply TSubRepr_Refl.
-      apply TEq_LadderAssocLR.
-    }
-    apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]).
-    apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]).
-    apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]).
-    var_typing.
-    var_typing.
-    apply T_Descend with (τ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
-    repr_subtype.
-    var_typing.
-    repr_subtype.
-    apply id_morphism_path.
-    var_typing.
-    apply id_morphism_path.
-
-  - apply T_Let with (σ:=[< $"Angle"$~$"Turns"$~$"ℝ"$ -> $"ℝ"$ >]).
-    apply T_Abs.
-    * apply T_Descend with (τ:=[<$"Angle"$~$"Turns"$~$"ℝ"$>]).
-      2: repr_subtype.
-      var_typing.
-
-    * apply T_App with (σ':=[<($"Angle"$~$"Degrees"$)~$"ℝ"$>])  (σ:=[<($"Angle"$~$"Turns"$)~$"ℝ"$>]) (τ:=[<$"ℝ"$>]).
-      apply T_DescendImplicit with (τ:=[< $"Angle"$~$"Turns"$~$"ℝ"$ -> $"ℝ"$ >]).
-      2: {
-        apply TSubRepr_Refl.
-        apply TEq_SubFun.
-        apply TEq_LadderAssocRL.
-        apply TEq_Refl.
-      }
-      var_typing.
-
-      apply T_Ascend with (τ':=[<$"Angle"$~$"Degrees"$>]) (τ:=[<$"ℝ"$>]).
-      var_typing.
-
-      apply M_Single with (h:="deg2turns"%string).
-      var_typing.
-
-  - admit.
-  (*
-  - apply Expand_MorphAbs.
-    * apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]).
-      2: repr_subtype.
-      apply T_Ascend with (τ':=[<$"Angle"$~$"Turns"$>]) (τ:=[<$"ℝ"$>]).
-      apply T_App with (σ:=[<$"ℝ"$>]) (σ':=[<$"ℝ"$>]).
-      apply T_App with (σ:=[<$"ℝ"$>]) (σ':=[<$"ℝ"$>]).
-      auto using T_Var, C_shuffle, C_take.
-      apply T_Descend with (τ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
-      2: repr_subtype.
-      var_typing.
-      apply id_morphism_path.
-      var_typing.
-      apply id_morphism_path.
-
-    * apply T_Abs.
-      apply T_DescendImplicit with (τ:=[< ($"Angle"$~$"Turns"$) ~ $"ℝ"$ >]).
-      2: repr_subtype.
-      apply T_Ascend with (τ':=[<$"Angle"$~$"Turns"$>]) (τ:=[<$"ℝ"$>]).
-      apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]).
-      apply T_App with (σ':=[<$"ℝ"$>]) (σ:=[<$"ℝ"$>]).
-      var_typing.
-      apply T_Descend with [<$"Angle"$~$"Degrees"$~$"ℝ"$>].
-      2: repr_subtype.
-      var_typing.
-      apply id_morphism_path.
-      var_typing.
-      apply id_morphism_path.
-
-    * apply Expand_Ascend.
-*)
-  - admit.
-Admitted.