Require Import List.
Require Import String.
Open Scope string_scope.
Inductive expr : Set :=
| Var : string -> expr
| App : expr -> expr -> expr
| Lam : string -> expr -> expr.
Coercion Var : string >-> expr.
Notation "X @ Y" := (App X Y) (at level 49).
Notation "\ X , Y" := (Lam X Y) (at level 50).
Check (\"x", \"y", "x").
Check (\"x", \"y", "y").
Check ((\"x", "x" @ "x") @ (\"x", "x" @ "x")).
Require Import String.
Open Scope string_scope.
Inductive expr : Set :=
| Var : string -> expr
| App : expr -> expr -> expr
| Lam : string -> expr -> expr.
Coercion Var : string >-> expr.
Notation "X @ Y" := (App X Y) (at level 49).
Notation "\ X , Y" := (Lam X Y) (at level 50).
Check (\"x", \"y", "x").
Check (\"x", \"y", "y").
Check ((\"x", "x" @ "x") @ (\"x", "x" @ "x")).
e1e2/x = e3
Inductive Subst : expr -> expr -> string ->
expr -> Prop :=
| SubstVar_same:
forall e x,
Subst (Var x) e x e
| SubstVar_diff:
forall e x1 x2,
x1 <> x2 ->
Subst (Var x1) e x2 (Var x1)
| SubstApp:
forall e1 e2 e x e1´ e2´,
Subst e1 e x e1´ ->
Subst e2 e x e2´ ->
Subst (App e1 e2) e x (App e1´ e2´)
| SubstLam_same:
forall e1 x e,
Subst (Lam x e1) e x (Lam x e1)
| SubstLam_diff:
forall e1 x1 x2 e e1´,
x1 <> x2 ->
Subst e1 e x2 e1´ ->
Subst (Lam x1 e1) e x2 (Lam x1 e1´).
Lemma subst_test_1:
Subst (\"x", "y") "z" "y"
(\"x", "z").
Proof.
apply SubstLam_diff.
- discriminate.
- apply SubstVar_same.
Qed.
Lemma subst_test_2:
Subst (\"x", "x") "z" "x"
(\"x", "x").
Proof.
apply SubstLam_same.
Qed.
expr -> Prop :=
| SubstVar_same:
forall e x,
Subst (Var x) e x e
| SubstVar_diff:
forall e x1 x2,
x1 <> x2 ->
Subst (Var x1) e x2 (Var x1)
| SubstApp:
forall e1 e2 e x e1´ e2´,
Subst e1 e x e1´ ->
Subst e2 e x e2´ ->
Subst (App e1 e2) e x (App e1´ e2´)
| SubstLam_same:
forall e1 x e,
Subst (Lam x e1) e x (Lam x e1)
| SubstLam_diff:
forall e1 x1 x2 e e1´,
x1 <> x2 ->
Subst e1 e x2 e1´ ->
Subst (Lam x1 e1) e x2 (Lam x1 e1´).
Lemma subst_test_1:
Subst (\"x", "y") "z" "y"
(\"x", "z").
Proof.
apply SubstLam_diff.
- discriminate.
- apply SubstVar_same.
Qed.
Lemma subst_test_2:
Subst (\"x", "x") "z" "x"
(\"x", "x").
Proof.
apply SubstLam_same.
Qed.
Call By Name
e1 --> e1' --------------------- e1 e2 --> e1' e2 ----------------------------- (\x. e1) e2 --> e1[e2/x]
Inductive step_cbn : expr -> expr -> Prop :=
| CBN_crunch:
forall e1 e1´ e2,
step_cbn e1 e1´ ->
step_cbn (App e1 e2) (App e1´ e2)
| CBN_subst:
forall x e1 e2 e1´,
Subst e1 e2 x e1´ ->
step_cbn (App (Lam x e1) e2) e1´.
Notation "e1 ==> e2" := (step_cbn e1 e2) (at level 51).
Lemma sstep_test_1:
(\"x", "x") @ "z" ==> "z".
Proof.
apply CBN_subst.
apply SubstVar_same.
Qed.
Lemma Lam_nostep_cbn:
forall x e1 e2,
~ (\x, e1 ==> e2).
Proof.
intros. intro. inversion H.
Qed.
Ltac inv H := inversion H; subst.
careful to make IH sufficiently strong
Lemma Subst_det:
forall e1 e2 x e3,
Subst e1 e2 x e3 ->
forall e3´,
Subst e1 e2 x e3´ ->
e3 = e3´.
Proof.
induction 1; intros.
- inv H; auto. congruence.
- inv H0; auto. congruence.
- inv H1.
apply IHSubst1 in H4.
apply IHSubst2 in H8.
subst; auto.
- inv H; auto. congruence.
- inv H1; auto. congruence.
apply IHSubst in H8; subst; auto.
Qed.
Lemma step_cbn_det:
forall e e1,
e ==> e1 ->
forall e2,
e ==> e2 ->
e1 = e2.
Proof.
induction 1; intros.
- inv H0.
+ f_equal. apply IHstep_cbn; auto.
+ exfalso. apply Lam_nostep_cbn in H; auto.
- inv H0.
+ exfalso. apply Lam_nostep_cbn in H4; auto.
+ eapply Subst_det; eauto.
Qed.
forall e1 e2 x e3,
Subst e1 e2 x e3 ->
forall e3´,
Subst e1 e2 x e3´ ->
e3 = e3´.
Proof.
induction 1; intros.
- inv H; auto. congruence.
- inv H0; auto. congruence.
- inv H1.
apply IHSubst1 in H4.
apply IHSubst2 in H8.
subst; auto.
- inv H; auto. congruence.
- inv H1; auto. congruence.
apply IHSubst in H8; subst; auto.
Qed.
Lemma step_cbn_det:
forall e e1,
e ==> e1 ->
forall e2,
e ==> e2 ->
e1 = e2.
Proof.
induction 1; intros.
- inv H0.
+ f_equal. apply IHstep_cbn; auto.
+ exfalso. apply Lam_nostep_cbn in H; auto.
- inv H0.
+ exfalso. apply Lam_nostep_cbn in H4; auto.
+ eapply Subst_det; eauto.
Qed.
Call By Value
v ::= \ x . e e1 --> e1' --------------------- e1 e2 --> e1' e2 e2 --> e2' --------------------- v e2 --> v e2' ----------------------------- (\x. e1) v --> e1[v/x]
Inductive value : expr -> Prop :=
| VLam :
forall x e,
value (Lam x e).
Inductive step_cbv : expr -> expr -> Prop :=
| CBV_crunch_l:
forall e1 e1´ e2,
step_cbv e1 e1´ ->
step_cbv (App e1 e2) (App e1´ e2)
| CBV_crunch_r:
forall v e2 e2´,
value v ->
step_cbv e2 e2´ ->
step_cbv (App v e2) (App v e2´)
| CBV_subst:
forall x e1 v e1´,
value v ->
Subst e1 v x e1´ ->
step_cbv (App (Lam x e1) v) e1´.
Notation "e1 --> e2" := (step_cbv e1 e2) (at level 51).
This page has been generated by coqdoc