rename term types to expr_term and type_term and type_abs->type_univ, type_app->type_spec

coq/bbencode.v

@@ -1,9 +1,17 @@
+From Coq Require Import Strings.String.
+Require Import terms.
+Require Import subst.
+Require Import smallstep.
+
+Include Terms.
+Include Subst.
+Include Smallstep.
 
 
 (*  let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
  *                ∀α.(α->α)->α->α
 *)
-Definition bb_zero : expr :=
+Definition bb_zero : expr_term :=
   (expr_ty_abs "α"
     (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
       (expr_tm_abs "z" (type_var "α")
@@ -11,7 +19,7 @@ Definition bb_zero : expr :=
 
 (*  let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
 *)
-Definition bb_one : expr :=
+Definition bb_one : expr_term :=
   (expr_ty_abs "α"
     (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
       (expr_tm_abs "z" (type_var "α")
@@ -19,21 +27,21 @@ Definition bb_one : expr :=
 
 (*  let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
 *)
-Definition bb_two : expr :=
+Definition bb_two : expr_term :=
   (expr_ty_abs "α"
     (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
       (expr_tm_abs "z" (type_var "α")
         (expr_tm_app (expr_var "s") (expr_tm_app (expr_var "s") (expr_var "z")))))).
 
 
-Definition bb_succ : expr :=
-  (expr_tm_abs "n" (type_rung (type_id "ℕ")
-                    (type_rung (type_id "BBNat")
-                     (type_abs "α"
+Definition bb_succ : expr_term :=
+  (expr_tm_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_rung (type_id "ℕ") (type_id "BBNat"))
+       (expr_ascend (type_ladder (type_id "ℕ") (type_id "BBNat"))
           (expr_ty_abs "α"
             (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
               (expr_tm_abs "z" (type_var "α")
@@ -43,17 +51,17 @@ Definition bb_succ : expr :=
                       (expr_var "s"))
                     (expr_var "z")))))))).
 
-Definition e1 : expr :=
-  (expr_let "bb-zero" (type_rung (type_id "ℕ")
-                        (type_rung (type_id "BBNat")
-                          (type_abs "α"
+Definition e1 : expr_term :=
+  (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_tm_app (expr_tm_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
   ).
 
-Definition t1 : expr := (expr_tm_app (expr_var "x") (expr_var "x")).
+Definition t1 : expr_term := (expr_tm_app (expr_var "x") (expr_var "x")).
 
 Compute (expr_subst "x"
     (expr_ty_abs "α" (expr_tm_abs "a" (type_var "α") (expr_var "a")))

coq/equiv.v

@@ -40,42 +40,42 @@ Module Equiv.
 (** Define all rewrite steps *)
 
 Reserved Notation "S '-->distribute-ladder' T" (at level 40).
-Inductive type_distribute_ladder : ladder_type -> ladder_type -> Prop :=
+Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
   | L_DistributeOverApp : forall x y y',
-    (type_app x (type_rung y y'))
+    (type_spec x (type_ladder y y'))
     -->distribute-ladder
-    (type_rung (type_app x y) (type_app x y'))
+    (type_ladder (type_spec x y) (type_spec x y'))
 
   | L_DistributeOverFun1 : forall x x' y,
-    (type_fun (type_rung x x') y)
+    (type_fun (type_ladder x x') y)
     -->distribute-ladder
-    (type_rung (type_fun x y) (type_fun x' y))
+    (type_ladder (type_fun x y) (type_fun x' y))
 
   | L_DistributeOverFun2 : forall x y y',
-    (type_fun x (type_rung y y'))
+    (type_fun x (type_ladder y y'))
     -->distribute-ladder
-    (type_rung (type_fun x y) (type_fun x y'))
+    (type_ladder (type_fun x y) (type_fun x y'))
 
 where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
 
 
 
 Reserved Notation "S '-->condense-ladder' T" (at level 40).
-Inductive type_condense_ladder : ladder_type -> ladder_type -> Prop :=
+Inductive type_condense_ladder : type_term -> type_term -> Prop :=
   | L_CondenseOverApp : forall x y y',
-    (type_rung (type_app x y) (type_app x y'))
+    (type_ladder (type_spec x y) (type_spec x y'))
     -->condense-ladder
-    (type_app x (type_rung y y'))
+    (type_spec x (type_ladder y y'))
 
   | L_CondenseOverFun1 : forall x x' y,
-    (type_rung (type_fun x y) (type_fun x' y))
+    (type_ladder (type_fun x y) (type_fun x' y))
     -->condense-ladder
-    (type_fun (type_rung x x') y)
+    (type_fun (type_ladder x x') y)
 
   | L_CondenseOverFun2 : forall x y y',
-    (type_rung (type_fun x y) (type_fun x y'))
+    (type_ladder (type_fun x y) (type_fun x y'))
     -->condense-ladder
-    (type_fun x (type_rung y y'))
+    (type_fun x (type_ladder y y'))
 
 where "S '-->condense-ladder' T" := (type_condense_ladder S T).
 
@@ -114,7 +114,7 @@ Qed.
 (** Define the equivalence relation as reflexive, transitive hull. *)
 
 Reserved Notation " S '===' T " (at level 40).
-Inductive type_eq : ladder_type -> ladder_type -> Prop :=
+Inductive type_eq : type_term -> type_term -> Prop :=
   | L_Refl : forall x,
     x === x
 
@@ -164,7 +164,7 @@ Proof.
 Qed.
 
 (** "flat" types do not contain ladders *)
-Inductive type_is_flat : ladder_type -> Prop :=
+Inductive type_is_flat : type_term -> Prop :=
   | FlatUnit : (type_is_flat type_unit)
   | FlatVar : forall x, (type_is_flat (type_var x))
   | FlatNum : forall x, (type_is_flat (type_num x))
@@ -172,7 +172,7 @@ Inductive type_is_flat : ladder_type -> Prop :=
   | FlatApp : forall x y,
     (type_is_flat x) ->
     (type_is_flat y) ->
-    (type_is_flat (type_app x y))
+    (type_is_flat (type_spec x y))
 
   | FlatFun : forall x y,
     (type_is_flat x) ->
@@ -181,31 +181,31 @@ Inductive type_is_flat : ladder_type -> Prop :=
 
   | FlatSub : forall x v,
     (type_is_flat x) ->
-    (type_is_flat (type_abs v x))
+    (type_is_flat (type_univ v x))
 .
 
 (** Ladder Normal Form:
     exhaustive application of -->distribute-ladder
  *)
-Inductive type_is_lnf : ladder_type -> Prop :=
-  | LNF : forall x : ladder_type,
-  (not (exists y:ladder_type, x -->distribute-ladder y))
+Inductive type_is_lnf : type_term -> Prop :=
+  | LNF : forall x : type_term,
+  (not (exists y:type_term, x -->distribute-ladder y))
   -> (type_is_lnf x)
 .
 
 (** Parameter Normal Form:
     exhaustive application of -->condense-ladder
 *)
-Inductive type_is_pnf : ladder_type -> Prop :=
-  | PNF : forall x : ladder_type,
-  (not (exists y:ladder_type, x -->condense-ladder y))
+Inductive type_is_pnf : type_term -> Prop :=
+  | PNF : forall x : type_term,
+  (not (exists y:type_term, x -->condense-ladder y))
   -> (type_is_pnf x)
 .
 
 (** Any term in LNF either is flat, or is a ladder T1~T2 where T1 is flat and T2 is in LNF *)
 Lemma lnf_shape :
-  forall τ:ladder_type,
-  (type_is_lnf τ) -> ((type_is_flat τ) \/ (exists τ1 τ2, τ = (type_rung τ1 τ2) /\ (type_is_flat τ1) /\ (type_is_lnf τ2)))
+  forall τ:type_term,
+  (type_is_lnf τ) -> ((type_is_flat τ) \/ (exists τ1 τ2, τ = (type_ladder τ1 τ2) /\ (type_is_flat τ1) /\ (type_is_lnf τ2)))
 .
 Proof.
   intros τ H.
@@ -252,7 +252,9 @@ Proof.
   apply LNF.
   admit.
   
-  exists (type_abs s t).
+  admit.
+  
+  exists (type_univ s t).
   split. apply L_Refl.
   apply LNF.
   
@@ -280,7 +282,7 @@ Admitted.
  *)
 
 Example example_flat_type :
-    (type_is_flat (type_app (type_id "PosInt") (type_num 10))).
+    (type_is_flat (type_spec (type_id "PosInt") (type_num 10))).
 Proof.
     apply FlatApp.
     apply FlatId.
@@ -289,16 +291,16 @@ Qed.
 
 Example example_lnf_type :
     (type_is_lnf
-    (type_rung (type_app (type_id "Seq") (type_id "Char"))
-               (type_app (type_id "Seq") (type_id "Byte")))).
+    (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
+               (type_spec (type_id "Seq") (type_id "Byte")))).
 Proof.
 Admitted.
 
 Example example_type_eq :
-    (type_app (type_id "Seq") (type_rung (type_id "Char") (type_id "Byte")))
+    (type_spec (type_id "Seq") (type_ladder (type_id "Char") (type_id "Byte")))
     ===
-    (type_rung (type_app (type_id "Seq") (type_id "Char"))
-               (type_app (type_id "Seq") (type_id "Byte"))).
+    (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
+               (type_spec (type_id "Seq") (type_id "Byte"))).
 Proof.
   apply L_Distribute.
   apply L_DistributeOverApp.

coq/smallstep.v

@@ -11,7 +11,7 @@ Reserved Notation " s '-->α' t " (at level 40).
 Reserved Notation " s '-->β' t " (at level 40).
 Reserved Notation " s '-->δ' t " (at level 40).
 
-Inductive beta_step : expr -> expr -> Prop :=
+Inductive beta_step : expr_term -> expr_term -> Prop :=
   | E_AppLeft : forall e1 e1' e2,
     e1 -->β e1' ->
     (expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
@@ -43,7 +43,7 @@ Notation " s -->β* t " := (multi beta_step s t) (at level 40).
 *)
 
 (*
-Inductive delta_expand : expr -> expr -> Prop :=
+Inductive delta_expand : expr_term -> expr_term -> Prop :=
   | E_ImplicitCast
   (expr_tm_app e1 e2)
 *)

coq/subst.v

@@ -6,18 +6,18 @@ Include Terms.
 Module Subst.
 
 (* scoped variable substitution in type terms *)
-Fixpoint type_subst (v:string) (n:ladder_type) (t0:ladder_type) :=
+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_abs x t => if (eqb v x) then t0 else type_abs x (type_subst v n t)
-  | type_app t1 t2 => (type_app (type_subst v n t1) (type_subst v n t2))
   | type_fun t1 t2 => (type_fun (type_subst v n t1) (type_subst v n t2))
-  | type_rung t1 t2 => (type_rung (type_subst v n t1) (type_subst v n t2))
+  | type_univ x t => if (eqb v x) then t0 else type_univ x (type_subst v n t)
+  | type_spec t1 t2 => (type_spec (type_subst v n t1) (type_subst v n t2))
+  | type_ladder t1 t2 => (type_ladder (type_subst v n t1) (type_subst v n t2))
   | t => t
   end.
 
 (* scoped variable substitution, replaces free occurences of v with n in expression e *)
-Fixpoint expr_subst (v:string) (n:expr) (e0:expr) :=
+Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
   match e0 with
   | expr_var name => if (eqb v name) then n else e0
   | expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
@@ -30,13 +30,12 @@ Fixpoint expr_subst (v:string) (n:expr) (e0:expr) :=
   end.
 
 (* replace only type variables in expression *)
-Fixpoint expr_specialize (v:string) (n:ladder_type) (e0:expr) :=
+Fixpoint expr_specialize (v:string) (n:type_term) (e0:expr_term) :=
   match e0 with
   | expr_ty_app e t => expr_ty_app (expr_specialize v n e) (type_subst v n t)
   | expr_ascend t e => expr_ascend (type_subst v n t) (expr_specialize v n e)
   | expr_descend t e => expr_descend (type_subst v n t) (expr_specialize v n e)
   | e => e
   end.
-  
-  
+
 End Subst.

coq/terms.v

@@ -7,32 +7,31 @@ From Coq Require Import Strings.String.
 Module Terms.
 
 (* types *)
-Inductive ladder_type : Type :=
-  | type_unit : ladder_type
-  | type_id : string -> ladder_type
-  | type_var : string -> ladder_type
-  | type_num : nat -> ladder_type
-  | type_abs : string -> ladder_type -> ladder_type
-  | type_app : ladder_type -> ladder_type -> ladder_type
-  | type_fun : ladder_type -> ladder_type -> ladder_type
-  | type_rung : ladder_type -> ladder_type -> ladder_type
+Inductive type_term : Type :=
+  | type_unit : type_term
+  | type_id : string -> type_term
+  | type_var : string -> type_term
+  | type_num : nat -> type_term
+  | type_fun : type_term -> type_term -> type_term
+  | type_univ : string -> type_term -> type_term
+  | type_spec : type_term -> type_term -> type_term
+  | type_ladder : type_term -> type_term -> type_term
 .
 
 (* expressions *)
-Inductive expr : Type :=
-  | expr_var : string -> expr
-  | expr_ty_abs : string -> expr -> expr
-  | expr_ty_app : expr -> ladder_type -> expr
-  | expr_tm_abs : string -> ladder_type -> expr -> expr
-  | expr_tm_app : expr -> expr -> expr
-  | expr_let : string -> ladder_type -> expr -> expr -> expr
-  | expr_ascend : ladder_type -> expr -> expr
-  | expr_descend : ladder_type -> expr -> expr
+Inductive expr_term : Type :=
+  | expr_var : string -> expr_term
+  | expr_ty_abs : string -> expr_term -> expr_term
+  | expr_ty_app : expr_term -> type_term -> expr_term
+  | expr_tm_abs : string -> type_term -> expr_term -> expr_term
+  | expr_tm_app : 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
 .
 
-Coercion type_var : string >-> ladder_type.
-Coercion expr_var : string >-> expr.
-
+Coercion type_var : string >-> type_term.
+Coercion expr_var : string >-> expr_term.
 
 (*
 Notation "( x )" := x (at level 70).

coq/typing.v

@@ -3,19 +3,19 @@
  *)
 From Coq Require Import Strings.String.
 Require Import terms.
-
+Require Import subst.
 Include Terms.
-
+Include Subst.
 
 Module Typing.
 
 Inductive context : Type :=
-  | ctx_assign : string -> ladder_type -> context -> context
+  | ctx_assign : string -> type_term -> context -> context
   | ctx_empty : context
 .
 
-Inductive context_contains : context -> string -> ladder_type -> Prop :=
-  | C_take : forall (x:string) (X:ladder_type) (Γ: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) ->
@@ -48,7 +48,7 @@ where "Γ '|-' x '\in' X" := (expr_type Γ x X).
 Example typing1 :
   ctx_empty |-
   (expr_ty_abs "T" (expr_tm_abs "x" (type_var "T") (expr_var "x"))) \in
-    (type_abs "T" (type_fun (type_var "T") (type_var "T"))).
+    (type_univ "T" (type_fun (type_var "T") (type_var "T"))).
 Proof.
 Admitted.