senvas/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

coq: rename expr_term constructors: remove 'tm' prefix

Browse source
This commit is contained in:
Michael Sippel 2024-08-22 01:04:40 +02:00
parent 61f1234fcc
commit 39f312b401
Signed by: senvas
GPG key ID: F96CF119C34B64A6
5 changed files with 48 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
coq/bbencode.v
View file

@ -1,4 +1,5 @@
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import smallstep.
@ -7,35 +8,37 @@ 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 :=
(expr_ty_abs "α"
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
(expr_tm_abs "z" (type_var "α")
(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_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
(expr_tm_abs "z" (type_var "α")
(expr_tm_app (expr_var "s") (expr_var "z"))))).
(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_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")))))).
(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_tm_abs "n" (type_ladder (type_id "ℕ")
(expr_abs "n" (type_ladder (type_id "ℕ")
(type_ladder (type_id "BBNat")
(type_univ "α"
(type_fun (type_fun (type_var "α") (type_var "α"))
@ -43,10 +46,10 @@ Definition bb_succ : expr_term :=
(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 "α")
(expr_tm_app (expr_var "s")
(expr_tm_app (expr_tm_app
(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")))))))).
@ -58,25 +61,25 @@ Definition e1 : expr_term :=
(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"))
(expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
).
Definition t1 : expr_term := (expr_tm_app (expr_var "x") (expr_var "x")).
Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).
Compute (expr_subst "x"
(expr_ty_abs "α" (expr_tm_abs "a" (type_var "α") (expr_var "a")))
(expr_ty_abs "α" (expr_abs "a" (type_var "α") (expr_var "a")))
bb_one
).
Example example_let_reduction :
e1 -->β (expr_tm_app (expr_tm_app (expr_var "+") bb_zero) bb_zero).
e1 -->β (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
Proof.
apply E_AppLet.
Qed.
Compute (expr_tm_app bb_succ bb_zero) -->β bb_one.
Compute (expr_app bb_succ bb_zero) -->β bb_one.
Example example_succ :
(expr_tm_app bb_succ bb_zero) -->β bb_one.
(expr_app bb_succ bb_zero) -->β bb_one.
Proof.
Admitted.

4
coq/smallstep.v
View file

@ -16,11 +16,11 @@ Reserved Notation " s '-->eval' t " (at level 40).
Inductive beta_step : expr_term -> expr_term -> Prop :=
| E_App1 : forall e1 e1' e2,
e1 -->β e1' ->
(expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
(expr_app e1 e2) -->β (expr_app e1' e2)
| E_App2 : forall e1 e2 e2',
e2 -->β e2' ->
(expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
(expr_app e1 e2) -->β (expr_app e1 e2')
| E_TypApp : forall e e' τ,
e -->β e' ->

6
coq/subst.v
View file

@ -112,9 +112,9 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
| 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)
| expr_ty_app e t => expr_ty_app (expr_subst v n e) t
| expr_tm_abs x t e => if (eqb v x) then e0 else expr_tm_abs x t (expr_subst v n e)
| expr_tm_abs_morph x t e => if (eqb v x) then e0 else expr_tm_abs_morph x t (expr_subst v n e)
| expr_tm_app e a => expr_tm_app (expr_subst v n e) (expr_subst v n a)
| 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 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)

18
coq/terms.v
View file

@ -22,9 +22,9 @@ 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_abs_morph : string -> type_term -> expr_term -> expr_term
| expr_tm_app : expr_term -> expr_term -> expr_term
| 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 -> type_term -> expr_term -> expr_term -> expr_term
| expr_ascend : type_term -> expr_term -> expr_term
| expr_descend : type_term -> expr_term -> expr_term
@ -32,8 +32,8 @@ Inductive expr_term : Type :=
(* values *)
Inductive is_value : expr_term -> Prop :=
| V_ValAbs : forall x τ e,
(is_value (expr_tm_abs x τ e))
| V_Abs : forall x τ e,
(is_value (expr_abs x τ e))
| V_TypAbs : forall τ e,
(is_value (expr_ty_abs τ e))
@ -43,6 +43,8 @@ Inductive is_value : expr_term -> Prop :=
(is_value (expr_ascend τ e))
.
Declare Scope ladder_type_scope.
Declare Scope ladder_expr_scope.
Declare Custom Entry ladder_type.
@ -71,10 +73,14 @@ 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_tm_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 "'λ' 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 0, t constr, e custom ladder_expr at level 80).
(* EXAMPLES *)
Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.

15
coq/typing.v
View file

@ -52,12 +52,12 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
(context_contains Γ x σ) ->
Γ |- t \is τ ->
Γ |- (expr_tm_abs x σ t) \is (type_fun σ τ)
Γ |- (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_tm_app f a) \is τ
Γ |- (expr_app f a) \is τ
| T_Sub : forall Γ x τ τ',
Γ |- x \is τ ->
@ -88,17 +88,17 @@ Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
| T_CompatMorphAbs : forall Γ x t τ τ',
Γ |- t \compatible τ ->
(τ ~<= τ') ->
Γ |- (expr_tm_abs_morph x τ t) \compatible (type_morph τ τ')
Γ |- (expr_morph x τ t) \compatible (type_morph τ τ')
| T_CompatAbs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
(context_contains Γ x σ) ->
Γ |- t \compatible τ ->
Γ |- (expr_tm_abs x σ t) \compatible (type_fun σ τ)
Γ |- (expr_abs x σ t) \compatible (type_fun σ τ)
| T_CompatApp : forall Γ f a σ τ,
(Γ |- f \compatible (type_fun σ τ)) ->
(Γ |- a \compatible σ) ->
(Γ |- (expr_tm_app f a) \compatible τ)
(Γ |- (expr_app f a) \compatible τ)
| T_CompatImplicitCast : forall Γ h x τ τ',
(context_contains Γ h (type_morph τ τ')) ->
@ -112,10 +112,13 @@ Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
Definition is_well_typed (e:expr_term) : Prop :=
exists Γ τ,
Γ |- e \compatible τ
.
(* Examples *)
Example typing1 :
forall Γ,
(context_contains Γ "x" [ %"T"% ]) ->