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

This commit is contained in:
Michael Sippel 2024-07-25 11:04:56 +02:00
parent ec1a2ab4a4
commit f2a5d4a11b
Signed by: senvas
GPG key ID: F96CF119C34B64A6
6 changed files with 89 additions and 81 deletions

View file

@ -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")
Definition bb_succ : expr_term :=
(expr_tm_abs "n" (type_ladder (type_id "")
(type_ladder (type_id "BBNat")
(type_abs "α"
(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,9 +51,9 @@ 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")
Definition e1 : expr_term :=
(expr_let "bb-zero" (type_ladder (type_id "")
(type_ladder (type_id "BBNat")
(type_abs "α"
(type_fun (type_fun (type_var "α") (type_var "α"))
(type_fun (type_var "α") (type_var "α"))))))
@ -53,7 +61,7 @@ Definition e1 : expr :=
(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")))

View file

@ -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.

View file

@ -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)
*)

View file

@ -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,7 +30,7 @@ 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)
@ -38,5 +38,4 @@ Fixpoint expr_specialize (v:string) (n:ladder_type) (e0:expr) :=
| e => e
end.
End Subst.

View file

@ -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).

View file

@ -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.