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

coq: smallstep: define delta expansion

Browse source
This commit is contained in:
Michael Sippel 2024-07-25 12:42:32 +02:00
parent ec955c3c19
commit 13165a7951
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 42 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
coq/smallstep.v
View file

@ -1,51 +1,76 @@
From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import typing.
Include Terms.
Include Subst.
Include Typing.
Module Smallstep.
Reserved Notation " s '-->α' t " (at level 40).
Reserved Notation " s '-->β' t " (at level 40).
Reserved Notation " s '-->δ' t " (at level 40).
Reserved Notation " s '-->eval' t " (at level 40).
Inductive beta_step : expr_term -> expr_term -> Prop :=
| E_AppLeft : forall e1 e1' e2,
| E_App1 : forall e1 e1' e2,
e1 -->β e1' ->
(expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
| E_AppRight : forall e1 e2 e2',
| E_App2 : forall e1 e2 e2',
e2 -->β e2' ->
(expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
| E_AppTmAbs : forall x τ e a,
(expr_tm_app (expr_tm_abs x τ e) a) -->β (expr_subst x a e)
| E_TypApp : forall e e' τ,
e -->β e' ->
(expr_ty_app e τ) -->β (expr_ty_app e' τ)
| E_AppTyAbs : forall x e a,
| E_TypAppLam : forall x e a,
(expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
| E_AppLam : forall x τ e a,
(expr_tm_app (expr_tm_abs x τ e) a) -->β (expr_subst x a e)
| E_AppLet : forall x t e a,
(expr_let x t a e) -->β (expr_subst x a e)
where "s '-->β' t" := (beta_step s t).
(*
Inductive multi {X : Type} (R : relation X) : relation X :=
| multi_refl : forall (x : X), multi R x x
| multi_step : forall (x y z : X),
Inductive delta_step : expr_term -> expr_term -> Prop :=
| E_ImplicitCast : forall (Γ:context) (f:expr_term) (h:string) (a:expr_term) (τ:type_term) (s:type_term) (p:type_term),
(context_contains Γ h (type_morph p s)) ->
Γ |- f \is (type_fun s τ) ->
Γ |- a \is p ->
(expr_tm_app f a) -->δ (expr_tm_app f (expr_tm_app (expr_var h) a))
where "s '-->δ' t" := (delta_step s t).
Inductive eval_step : expr_term -> expr_term -> Prop :=
| E_Beta : forall s t,
(s -->β t) ->
(s -->eval t)
| E_Delta : forall s t,
(s -->δ t) ->
(s -->eval t)
where "s '-->eval' t" := (eval_step s t).
Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
| Multi_Refl : forall (x : X), multi R x x
| Multi_Step : forall (x y z : X),
R x y ->
multi R y z ->
multi R x z.
Notation " s -->β* t " := (multi beta_step s t) (at level 40).
*)
(*
Inductive delta_expand : expr_term -> expr_term -> Prop :=
| E_ImplicitCast
(expr_tm_app e1 e2)
*)
Notation " s -->δ* t " := (multi delta_step s t) (at level 40).
Notation " s -->eval* t " := (multi eval_step s t) (at level 40).
End Smallstep.