Compare commits
3 commits
f2a5d4a11b
...
13165a7951
Author | SHA1 | Date | |
---|---|---|---|
13165a7951 | |||
ec955c3c19 | |||
292234c247 |
4 changed files with 47 additions and 19 deletions
|
@ -37,7 +37,7 @@ Definition bb_two : expr_term :=
|
||||||
Definition bb_succ : expr_term :=
|
Definition bb_succ : expr_term :=
|
||||||
(expr_tm_abs "n" (type_ladder (type_id "ℕ")
|
(expr_tm_abs "n" (type_ladder (type_id "ℕ")
|
||||||
(type_ladder (type_id "BBNat")
|
(type_ladder (type_id "BBNat")
|
||||||
(type_abs "α"
|
(type_univ "α"
|
||||||
(type_fun (type_fun (type_var "α") (type_var "α"))
|
(type_fun (type_fun (type_var "α") (type_var "α"))
|
||||||
(type_fun (type_var "α") (type_var "α"))))))
|
(type_fun (type_var "α") (type_var "α"))))))
|
||||||
|
|
||||||
|
@ -54,7 +54,7 @@ Definition bb_succ : expr_term :=
|
||||||
Definition e1 : expr_term :=
|
Definition e1 : expr_term :=
|
||||||
(expr_let "bb-zero" (type_ladder (type_id "ℕ")
|
(expr_let "bb-zero" (type_ladder (type_id "ℕ")
|
||||||
(type_ladder (type_id "BBNat")
|
(type_ladder (type_id "BBNat")
|
||||||
(type_abs "α"
|
(type_univ "α"
|
||||||
(type_fun (type_fun (type_var "α") (type_var "α"))
|
(type_fun (type_fun (type_var "α") (type_var "α"))
|
||||||
(type_fun (type_var "α") (type_var "α"))))))
|
(type_fun (type_var "α") (type_var "α"))))))
|
||||||
bb_zero
|
bb_zero
|
||||||
|
|
|
@ -1,51 +1,76 @@
|
||||||
From Coq Require Import Strings.String.
|
From Coq Require Import Strings.String.
|
||||||
Require Import terms.
|
Require Import terms.
|
||||||
Require Import subst.
|
Require Import subst.
|
||||||
|
Require Import typing.
|
||||||
|
|
||||||
Include Terms.
|
Include Terms.
|
||||||
Include Subst.
|
Include Subst.
|
||||||
|
Include Typing.
|
||||||
|
|
||||||
Module Smallstep.
|
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 '-->δ' 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 :=
|
Inductive beta_step : expr_term -> expr_term -> Prop :=
|
||||||
| E_AppLeft : forall e1 e1' e2,
|
| E_App1 : forall e1 e1' e2,
|
||||||
e1 -->β e1' ->
|
e1 -->β e1' ->
|
||||||
(expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
|
(expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
|
||||||
|
|
||||||
| E_AppRight : forall e1 e2 e2',
|
| E_App2 : forall e1 e2 e2',
|
||||||
e2 -->β e2' ->
|
e2 -->β e2' ->
|
||||||
(expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
|
(expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
|
||||||
|
|
||||||
| E_AppTmAbs : forall x τ e a,
|
| E_TypApp : forall e e' τ,
|
||||||
(expr_tm_app (expr_tm_abs x τ e) a) -->β (expr_subst x a 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)
|
(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,
|
| E_AppLet : forall x t e a,
|
||||||
(expr_let x t a e) -->β (expr_subst x a e)
|
(expr_let x t a e) -->β (expr_subst x a e)
|
||||||
|
|
||||||
where "s '-->β' t" := (beta_step s t).
|
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
|
Inductive delta_step : expr_term -> expr_term -> Prop :=
|
||||||
| multi_step : forall (x y z : X),
|
|
||||||
|
| 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 ->
|
R x y ->
|
||||||
multi R y z ->
|
multi R y z ->
|
||||||
multi R x z.
|
multi R x z.
|
||||||
|
|
||||||
Notation " s -->β* t " := (multi beta_step s t) (at level 40).
|
Notation " s -->β* t " := (multi beta_step s t) (at level 40).
|
||||||
*)
|
Notation " s -->δ* t " := (multi delta_step s t) (at level 40).
|
||||||
|
Notation " s -->eval* t " := (multi eval_step s t) (at level 40).
|
||||||
(*
|
|
||||||
Inductive delta_expand : expr_term -> expr_term -> Prop :=
|
|
||||||
| E_ImplicitCast
|
|
||||||
(expr_tm_app e1 e2)
|
|
||||||
*)
|
|
||||||
|
|
||||||
End Smallstep.
|
End Smallstep.
|
||||||
|
|
|
@ -23,6 +23,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
|
||||||
| expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
|
| 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_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 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_tm_app e a => expr_tm_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_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_ascend t e => expr_ascend t (expr_subst v n e)
|
||||||
|
|
|
@ -15,6 +15,7 @@ Inductive type_term : Type :=
|
||||||
| type_fun : type_term -> type_term -> type_term
|
| type_fun : type_term -> type_term -> type_term
|
||||||
| type_univ : string -> type_term -> type_term
|
| type_univ : string -> type_term -> type_term
|
||||||
| type_spec : type_term -> type_term -> type_term
|
| type_spec : type_term -> type_term -> type_term
|
||||||
|
| type_morph : type_term -> type_term -> type_term
|
||||||
| type_ladder : type_term -> type_term -> type_term
|
| type_ladder : type_term -> type_term -> type_term
|
||||||
.
|
.
|
||||||
|
|
||||||
|
@ -24,6 +25,7 @@ Inductive expr_term : Type :=
|
||||||
| expr_ty_abs : string -> expr_term -> expr_term
|
| expr_ty_abs : string -> expr_term -> expr_term
|
||||||
| expr_ty_app : expr_term -> type_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 : 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_tm_app : expr_term -> expr_term -> expr_term
|
||||||
| expr_let : string -> type_term -> 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_ascend : type_term -> expr_term -> expr_term
|
||||||
|
|
Loading…
Reference in a new issue