mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
Rename samples subdirectories
This commit is contained in:
Joshua Peek
701
samples/Coq/Smallstep.v
Executable file
701
samples/Coq/Smallstep.v
Executable file
@@ -0,0 +1,701 @@
|
||||
Require Export Imp.
|
||||
Require Export Relations.
|
||||
|
||||
Inductive tm : Type :=
|
||||
| tm_const : nat -> tm
|
||||
| tm_plus : tm -> tm -> tm.
|
||||
|
||||
Tactic Notation "tm_cases" tactic(first) ident(c) :=
|
||||
first;
|
||||
[ Case_aux c "tm_const" | Case_aux c "tm_plus" ].
|
||||
|
||||
Module SimpleArith0.
|
||||
|
||||
Fixpoint eval (t : tm) : nat :=
|
||||
match t with
|
||||
| tm_const n => n
|
||||
| tm_plus a1 a2 => eval a1 + eval a2
|
||||
end.
|
||||
|
||||
End SimpleArith0.
|
||||
|
||||
Module SimpleArith1.
|
||||
|
||||
Reserved Notation " t '===>' n " (at level 50, left associativity).
|
||||
|
||||
Inductive eval : tm -> nat -> Prop :=
|
||||
| E_Const : forall n,
|
||||
tm_const n ===> n
|
||||
| E_Plus : forall t1 t2 n1 n2,
|
||||
t1 ===> n1 ->
|
||||
t2 ===> n2 ->
|
||||
tm_plus t1 t2 ===> plus n1 n2
|
||||
|
||||
where " t '===>' n " := (eval t n).
|
||||
|
||||
End SimpleArith1.
|
||||
|
||||
Reserved Notation " t '===>' t' " (at level 50, left associativity).
|
||||
|
||||
Inductive eval : tm -> tm -> Prop :=
|
||||
| E_Const : forall n1,
|
||||
tm_const n1 ===> tm_const n1
|
||||
| E_Plus : forall t1 n1 t2 n2,
|
||||
t1 ===> tm_const n1 ->
|
||||
t2 ===> tm_const n2 ->
|
||||
tm_plus t1 t2 ===> tm_const (plus n1 n2)
|
||||
where " t '===>' t' " := (eval t t').
|
||||
|
||||
Tactic Notation "eval_cases" tactic(first) ident(c) :=
|
||||
first;
|
||||
[ Case_aux c "E_Const" | Case_aux c "E_Plus" ].
|
||||
|
||||
Module SimpleArith2.
|
||||
|
||||
Reserved Notation " t '=>' t' " (at level 40).
|
||||
|
||||
Inductive step : tm -> tm -> Prop :=
|
||||
| ST_PlusConstConst : forall n1 n2,
|
||||
tm_plus (tm_const n1) (tm_const n2) => tm_const (plus n1 n2)
|
||||
| ST_Plus1 : forall t1 t1' t2,
|
||||
t1 => t1' ->
|
||||
tm_plus t1 t2 => tm_plus t1' t2
|
||||
| ST_Plus2 : forall n1 t2 t2',
|
||||
t2 => t2' ->
|
||||
tm_plus (tm_const n1) t2 => tm_plus (tm_const n1) t2'
|
||||
|
||||
where " t '=>' t' " := (step t t').
|
||||
|
||||
Tactic Notation "step_cases" tactic(first) ident(c) :=
|
||||
first;
|
||||
[ Case_aux c "ST_PlusConstConst"
|
||||
| Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
|
||||
|
||||
Example test_step_1 :
|
||||
tm_plus
|
||||
(tm_plus (tm_const 0) (tm_const 3))
|
||||
(tm_plus (tm_const 2) (tm_const 4))
|
||||
=>
|
||||
tm_plus
|
||||
(tm_const (plus 0 3))
|
||||
(tm_plus (tm_const 2) (tm_const 4)).
|
||||
Proof.
|
||||
apply ST_Plus1. apply ST_PlusConstConst. Qed.
|
||||
|
||||
Example test_step_2 :
|
||||
tm_plus
|
||||
(tm_const 0)
|
||||
(tm_plus
|
||||
(tm_const 2)
|
||||
(tm_plus (tm_const 0) (tm_const 3)))
|
||||
=>
|
||||
tm_plus
|
||||
(tm_const 0)
|
||||
(tm_plus
|
||||
(tm_const 2)
|
||||
(tm_const (plus 0 3))).
|
||||
Proof.
|
||||
apply ST_Plus2.
|
||||
simpl.
|
||||
apply ST_Plus2.
|
||||
apply ST_PlusConstConst.
|
||||
Qed.
|
||||
|
||||
Theorem step_deterministic:
|
||||
partial_function step.
|
||||
Proof.
|
||||
unfold partial_function. intros x y1 y2 Hy1 Hy2.
|
||||
generalize dependent y2.
|
||||
step_cases (induction Hy1) Case; intros y2 Hy2.
|
||||
Case "ST_PlusConstConst". step_cases (inversion Hy2) SCase.
|
||||
SCase "ST_PlusConstConst". reflexivity.
|
||||
SCase "ST_Plus1". inversion H2.
|
||||
SCase "ST_Plus2". inversion H2.
|
||||
Case "ST_Plus1". step_cases (inversion Hy2) SCase.
|
||||
SCase "ST_PlusConstConst". rewrite <- H0 in Hy1. inversion Hy1.
|
||||
SCase "ST_Plus1".
|
||||
rewrite <- (IHHy1 t1'0).
|
||||
reflexivity. assumption.
|
||||
SCase "ST_Plus2". rewrite <- H in Hy1. inversion Hy1.
|
||||
Case "ST_Plus2". step_cases (inversion Hy2) SCase.
|
||||
SCase "ST_PlusConstConst". rewrite <- H1 in Hy1. inversion Hy1.
|
||||
SCase "ST_Plus1". inversion H2.
|
||||
SCase "ST_Plus2".
|
||||
rewrite <- (IHHy1 t2'0).
|
||||
reflexivity. assumption. Qed.
|
||||
|
||||
End SimpleArith2.
|
||||
|
||||
Inductive value : tm -> Prop :=
|
||||
v_const: forall n, value (tm_const n).
|
||||
|
||||
Reserved Notation " t '=>' t' " (at level 40).
|
||||
|
||||
Inductive step : tm -> tm -> Prop :=
|
||||
| ST_PlusConstConst : forall n1 n2,
|
||||
tm_plus (tm_const n1) (tm_const n2)
|
||||
=> tm_const (plus n1 n2)
|
||||
| ST_Plus1 : forall t1 t1' t2,
|
||||
t1 => t1' ->
|
||||
tm_plus t1 t2 => tm_plus t1' t2
|
||||
| ST_Plus2 : forall v1 t2 t2',
|
||||
value v1 ->
|
||||
t2 => t2' ->
|
||||
tm_plus v1 t2 => tm_plus v1 t2'
|
||||
|
||||
where " t '=>' t' " := (step t t').
|
||||
|
||||
Tactic Notation "step_cases" tactic(first) ident(c) :=
|
||||
first;
|
||||
[ Case_aux c "ST_PlusConstConst"
|
||||
| Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
|
||||
|
||||
Theorem step_deterministic :
|
||||
partial_function step.
|
||||
Proof.
|
||||
unfold partial_function.
|
||||
intros x y1 y2 Hy1 Hy2.
|
||||
generalize dependent y2.
|
||||
step_cases (induction Hy1) Case; intros y2 Hy2.
|
||||
step_cases (inversion Hy2) SCase.
|
||||
reflexivity.
|
||||
|
||||
inversion H2.
|
||||
|
||||
inversion Hy2.
|
||||
subst.
|
||||
assumption.
|
||||
|
||||
subst.
|
||||
inversion H3.
|
||||
|
||||
subst.
|
||||
inversion H3.
|
||||
|
||||
step_cases (inversion Hy2) SCase.
|
||||
rewrite <- H0 in Hy1.
|
||||
inversion Hy1.
|
||||
|
||||
rewrite <- (IHHy1 t1'0).
|
||||
reflexivity.
|
||||
|
||||
assumption.
|
||||
|
||||
rewrite <- H in Hy1.
|
||||
rewrite <- H in H1.
|
||||
subst.
|
||||
inversion H1.
|
||||
subst.
|
||||
inversion Hy1.
|
||||
|
||||
step_cases (inversion Hy2) SCase.
|
||||
subst.
|
||||
inversion Hy1.
|
||||
|
||||
subst.
|
||||
inversion H.
|
||||
subst.
|
||||
inversion H3.
|
||||
|
||||
subst.
|
||||
inversion H2.
|
||||
subst.
|
||||
rewrite <- (IHHy1 t2'0).
|
||||
reflexivity.
|
||||
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Theorem strong_progress : forall t,
|
||||
value t \/ (exists t', t => t').
|
||||
Proof.
|
||||
tm_cases (induction t) Case.
|
||||
Case "tm_const". left. apply v_const.
|
||||
Case "tm_plus". right. inversion IHt1.
|
||||
SCase "l". inversion IHt2.
|
||||
SSCase "l". inversion H. inversion H0.
|
||||
exists (tm_const (plus n n0)).
|
||||
apply ST_PlusConstConst.
|
||||
SSCase "r". inversion H0 as [t' H1].
|
||||
exists (tm_plus t1 t').
|
||||
apply ST_Plus2. apply H. apply H1.
|
||||
SCase "r". inversion H as [t' H0].
|
||||
exists (tm_plus t' t2).
|
||||
apply ST_Plus1. apply H0. Qed.
|
||||
|
||||
Definition normal_form {X:Type} (R: relation X) (t: X) : Prop :=
|
||||
~ (exists t', R t t').
|
||||
|
||||
Lemma value_is_nf: forall t,
|
||||
value t -> normal_form step t.
|
||||
Proof.
|
||||
unfold normal_form. intros t H. inversion H.
|
||||
intros contra. inversion contra. inversion H1.
|
||||
Qed.
|
||||
|
||||
Lemma nf_is_value: forall t,
|
||||
normal_form step t -> value t.
|
||||
Proof.
|
||||
unfold normal_form. intros t H.
|
||||
assert (G: value t \/ (exists t', t => t')).
|
||||
SCase "Proof of assertion". apply strong_progress.
|
||||
inversion G.
|
||||
SCase "l". assumption.
|
||||
SCase "r". apply ex_falso_quodlibet. apply H. assumption. Qed.
|
||||
|
||||
Corollary nf_same_as_value : forall t,
|
||||
normal_form step t <-> value t.
|
||||
Proof.
|
||||
split. apply nf_is_value. apply value_is_nf.
|
||||
Qed.
|
||||
|
||||
Module Temp1.
|
||||
|
||||
Inductive value : tm -> Prop :=
|
||||
| v_const : forall n, value (tm_const n)
|
||||
| v_funny : forall t1 n2, (* <---- *)
|
||||
value (tm_plus t1 (tm_const n2)).
|
||||
|
||||
Reserved Notation " t '=>' t' " (at level 40).
|
||||
|
||||
Inductive step : tm -> tm -> Prop :=
|
||||
| ST_PlusConstConst : forall n1 n2,
|
||||
tm_plus (tm_const n1) (tm_const n2) => tm_const (plus n1 n2)
|
||||
| ST_Plus1 : forall t1 t1' t2,
|
||||
t1 => t1' ->
|
||||
tm_plus t1 t2 => tm_plus t1' t2
|
||||
| ST_Plus2 : forall v1 t2 t2',
|
||||
value v1 ->
|
||||
t2 => t2' ->
|
||||
tm_plus v1 t2 => tm_plus v1 t2'
|
||||
|
||||
where " t '=>' t' " := (step t t').
|
||||
|
||||
Lemma value_not_same_as_normal_form:
|
||||
exists t, value t /\ ~ normal_form step t.
|
||||
Proof.
|
||||
intros.
|
||||
unfold normal_form.
|
||||
exists (tm_plus (tm_plus (tm_const 1) (tm_const 2)) (tm_const 2)).
|
||||
split.
|
||||
apply v_funny.
|
||||
|
||||
unfold not.
|
||||
intros.
|
||||
apply H.
|
||||
exists (tm_plus (tm_const (1 + 2)) (tm_const 2)).
|
||||
apply ST_Plus1.
|
||||
apply ST_PlusConstConst.
|
||||
Qed.
|
||||
|
||||
End Temp1.
|
||||
|
||||
Module Temp2.
|
||||
|
||||
Inductive value : tm -> Prop :=
|
||||
| v_const : forall n, value (tm_const n).
|
||||
|
||||
(*Reserved Notation " t '===>' t' " (at level 40).*)
|
||||
|
||||
Inductive step : tm -> tm -> Prop :=
|
||||
| ST_Funny : forall n, (* <---- *)
|
||||
tm_const n ===> tm_plus (tm_const n) (tm_const 0)
|
||||
| ST_PlusConstConst : forall n1 n2,
|
||||
tm_plus (tm_const n1) (tm_const n2) ===> tm_const (plus n1 n2)
|
||||
| ST_Plus1 : forall t1 t1' t2,
|
||||
t1 ===> t1' ->
|
||||
tm_plus t1 t2 ===> tm_plus t1' t2
|
||||
| ST_Plus2 : forall v1 t2 t2',
|
||||
value v1 ->
|
||||
t2 ===> t2' ->
|
||||
tm_plus v1 t2 ===> tm_plus v1 t2'
|
||||
|
||||
where " t '===>' t' " := (step t t').
|
||||
|
||||
Lemma value_not_same_as_normal_form :
|
||||
exists t, value t /\ ~ normal_form step t.
|
||||
Proof.
|
||||
exists (tm_const 0).
|
||||
split.
|
||||
apply v_const.
|
||||
|
||||
unfold normal_form.
|
||||
unfold not.
|
||||
intro H.
|
||||
apply H.
|
||||
exists (tm_plus (tm_const 0) (tm_const 0)).
|
||||
apply ST_Funny.
|
||||
Qed.
|
||||
|
||||
End Temp2.
|
||||
|
||||
Module Temp3.
|
||||
|
||||
Inductive value : tm -> Prop :=
|
||||
| v_const : forall n, value (tm_const n).
|
||||
|
||||
(*Reserved Notation " t '===>' t' " (at level 40).*)
|
||||
|
||||
Inductive step : tm -> tm -> Prop :=
|
||||
| ST_PlusConstConst : forall n1 n2,
|
||||
tm_plus (tm_const n1) (tm_const n2) ===> tm_const (plus n1 n2)
|
||||
| ST_Plus1 : forall t1 t1' t2,
|
||||
t1 ===> t1' ->
|
||||
tm_plus t1 t2 ===> tm_plus t1' t2
|
||||
|
||||
where " t '===>' t' " := (step t t').
|
||||
|
||||
Lemma value_not_same_as_normal_form:
|
||||
exists t, ~ value t /\ normal_form step t.
|
||||
Proof.
|
||||
exists (tm_plus (tm_const 1) (tm_plus (tm_const 0) (tm_const 0))).
|
||||
split.
|
||||
intros H.
|
||||
inversion H.
|
||||
|
||||
unfold normal_form.
|
||||
intros H.
|
||||
inversion H.
|
||||
inversion H0.
|
||||
inversion H4.
|
||||
Qed.
|
||||
|
||||
End Temp3.
|
||||
|
||||
Module Temp4.
|
||||
Inductive tm : Type :=
|
||||
| tm_true : tm
|
||||
| tm_false : tm
|
||||
| tm_if : tm -> tm -> tm -> tm.
|
||||
|
||||
Inductive value : tm -> Prop :=
|
||||
| v_true : value tm_true
|
||||
| v_false : value tm_false.
|
||||
|
||||
Inductive step : tm -> tm -> Prop :=
|
||||
| ST_IfTrue : forall t1 t2,
|
||||
tm_if tm_true t1 t2 ===> t1
|
||||
| ST_IfFalse : forall t1 t2,
|
||||
tm_if tm_false t1 t2 ===> t2
|
||||
| ST_If : forall t1 t1' t2 t3,
|
||||
t1 ===> t1' ->
|
||||
tm_if t1 t2 t3 ===> tm_if t1' t2 t3
|
||||
|
||||
where " t '===>' t' " := (step t t').
|
||||
|
||||
Example bool_step_prop3 :
|
||||
tm_if
|
||||
(tm_if tm_true tm_true tm_true)
|
||||
(tm_if tm_true tm_true tm_true)
|
||||
tm_false
|
||||
===>
|
||||
tm_if
|
||||
tm_true
|
||||
(tm_if tm_true tm_true tm_true)
|
||||
tm_false.
|
||||
Proof.
|
||||
apply ST_If.
|
||||
apply ST_IfTrue.
|
||||
Qed.
|
||||
|
||||
Theorem strong_progress: forall t,
|
||||
value t \/ (exists t', t ===> t').
|
||||
Proof.
|
||||
induction t.
|
||||
left.
|
||||
constructor.
|
||||
|
||||
left.
|
||||
constructor.
|
||||
|
||||
right.
|
||||
inversion IHt1.
|
||||
inversion H.
|
||||
exists t2.
|
||||
apply ST_IfTrue.
|
||||
|
||||
exists t3.
|
||||
apply ST_IfFalse.
|
||||
|
||||
inversion H.
|
||||
exists (tm_if x t2 t3).
|
||||
apply ST_If.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Theorem step_deterministic :
|
||||
partial_function step.
|
||||
Proof.
|
||||
unfold partial_function.
|
||||
intros x y1 y2 Hy1 Hy2.
|
||||
generalize dependent y2.
|
||||
induction Hy1.
|
||||
intros.
|
||||
inversion Hy2.
|
||||
reflexivity.
|
||||
|
||||
subst.
|
||||
inversion H3.
|
||||
|
||||
intros.
|
||||
inversion Hy2.
|
||||
reflexivity.
|
||||
|
||||
inversion H3.
|
||||
|
||||
intros.
|
||||
inversion Hy2.
|
||||
subst.
|
||||
inversion Hy1.
|
||||
|
||||
subst.
|
||||
inversion Hy1.
|
||||
|
||||
subst.
|
||||
apply IHHy1 in H3.
|
||||
subst.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Module Temp5.
|
||||
|
||||
|
||||
Inductive step : tm -> tm -> Prop :=
|
||||
| ST_IfTrue : forall t1 t2,
|
||||
tm_if tm_true t1 t2 ===> t1
|
||||
| ST_IfFalse : forall t1 t2,
|
||||
tm_if tm_false t1 t2 ===> t2
|
||||
| ST_If : forall t1 t1' t2 t3,
|
||||
t1 ===> t1' ->
|
||||
tm_if t1 t2 t3 ===> tm_if t1' t2 t3
|
||||
| ST_ShortCut : forall v t,
|
||||
value v ->
|
||||
tm_if t v v ===> v
|
||||
|
||||
where " t '===>' t' " := (step t t').
|
||||
|
||||
Definition bool_step_prop4 :=
|
||||
tm_if
|
||||
(tm_if tm_true tm_true tm_true)
|
||||
tm_false
|
||||
tm_false
|
||||
===>
|
||||
tm_false.
|
||||
|
||||
Example bool_step_prop4_holds :
|
||||
bool_step_prop4.
|
||||
Proof.
|
||||
unfold bool_step_prop4.
|
||||
apply ST_ShortCut.
|
||||
constructor.
|
||||
Qed.
|
||||
|
||||
Theorem strong_progress: forall t,
|
||||
value t \/ (exists t', t ===> t').
|
||||
Proof.
|
||||
induction t.
|
||||
left.
|
||||
constructor.
|
||||
|
||||
left.
|
||||
constructor.
|
||||
|
||||
inversion IHt1.
|
||||
right.
|
||||
inversion H.
|
||||
exists t2.
|
||||
constructor.
|
||||
|
||||
exists t3.
|
||||
constructor.
|
||||
|
||||
right.
|
||||
inversion H.
|
||||
exists (tm_if x t2 t3).
|
||||
apply ST_If.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
End Temp5.
|
||||
End Temp4.
|
||||
|
||||
Definition stepmany := refl_step_closure step.
|
||||
|
||||
Notation " t '===>*' t' " := (stepmany t t') (at level 40).
|
||||
|
||||
Lemma test_stepmany_1:
|
||||
tm_plus
|
||||
(tm_plus (tm_const 0) (tm_const 3))
|
||||
(tm_plus (tm_const 2) (tm_const 4))
|
||||
===>*
|
||||
tm_const (plus (plus 0 3) (plus 2 4)).
|
||||
Proof.
|
||||
eapply rsc_step. apply ST_Plus1. apply ST_PlusConstConst.
|
||||
eapply rsc_step. apply ST_Plus2. apply v_const.
|
||||
apply ST_PlusConstConst.
|
||||
eapply rsc_step. apply ST_PlusConstConst.
|
||||
apply rsc_refl. Qed.
|
||||
|
||||
Lemma test_stepmany_2:
|
||||
tm_const 3 ===>* tm_const 3.
|
||||
Proof.
|
||||
eapply rsc_refl.
|
||||
Qed.
|
||||
|
||||
Lemma test_stepmany_3:
|
||||
tm_plus (tm_const 0) (tm_const 3)
|
||||
===>*
|
||||
tm_plus (tm_const 0) (tm_const 3).
|
||||
Proof.
|
||||
eapply rsc_refl.
|
||||
Qed.
|
||||
|
||||
Lemma test_stepmany_4:
|
||||
tm_plus
|
||||
(tm_const 0)
|
||||
(tm_plus
|
||||
(tm_const 2)
|
||||
(tm_plus (tm_const 0) (tm_const 3)))
|
||||
===>*
|
||||
tm_plus
|
||||
(tm_const 0)
|
||||
(tm_const (plus 2 (plus 0 3))).
|
||||
Proof.
|
||||
eapply rsc_step.
|
||||
apply ST_Plus2.
|
||||
apply v_const.
|
||||
|
||||
apply ST_Plus2.
|
||||
apply v_const.
|
||||
|
||||
apply ST_PlusConstConst.
|
||||
|
||||
eapply rsc_step.
|
||||
apply ST_Plus2.
|
||||
apply v_const.
|
||||
|
||||
apply ST_PlusConstConst.
|
||||
|
||||
eapply rsc_refl.
|
||||
Qed.
|
||||
|
||||
Definition step_normal_form := normal_form step.
|
||||
|
||||
Definition normal_form_of (t t' : tm) :=
|
||||
(t ===>* t' /\ step_normal_form t').
|
||||
|
||||
(*
|
||||
Theorem normal_forms_unique:
|
||||
partial_function normal_form_of.
|
||||
Proof.
|
||||
unfold partial_function. unfold normal_form_of. intros x y1 y2 P1 P2.
|
||||
destruct P1 as [P11 P12]. destruct P2 as [P21 P22].
|
||||
generalize dependent y2.
|
||||
|
||||
unfold step_normal_form in P12.
|
||||
unfold step_normal_form.
|
||||
unfold normal_form.
|
||||
unfold normal_form in P12.
|
||||
induction x.
|
||||
intros.
|
||||
unfold stepmany.
|
||||
inversion P11.
|
||||
subst.
|
||||
inversion P21.
|
||||
subst.
|
||||
reflexivity.
|
||||
|
||||
subst.
|
||||
inversion P21.
|
||||
reflexivity.
|
||||
|
||||
subst.
|
||||
inversion H1.
|
||||
|
||||
inversion H.
|
||||
*)
|
||||
|
||||
Definition normalizing {X:Type} (R:relation X) :=
|
||||
forall t, exists t',
|
||||
(refl_step_closure R) t t' /\ normal_form R t'.
|
||||
|
||||
Lemma stepmany_congr_1 : forall t1 t1' t2,
|
||||
t1 ===>* t1' ->
|
||||
tm_plus t1 t2 ===>* tm_plus t1' t2.
|
||||
Proof.
|
||||
intros t1 t1' t2 H.
|
||||
rsc_cases (induction H) Case.
|
||||
apply rsc_refl.
|
||||
|
||||
apply rsc_step with (tm_plus y t2).
|
||||
apply ST_Plus1.
|
||||
apply H.
|
||||
|
||||
apply IHrefl_step_closure.
|
||||
Qed.
|
||||
|
||||
Lemma stepmany_congr2 : forall t1 t2 t2',
|
||||
value t1 ->
|
||||
t2 ===>* t2' ->
|
||||
tm_plus t1 t2 ===>* tm_plus t1 t2'.
|
||||
Proof.
|
||||
intros t1 t2 t2'.
|
||||
intros H1.
|
||||
intros H2.
|
||||
induction H2.
|
||||
apply rsc_refl.
|
||||
|
||||
apply rsc_step with (tm_plus t1 y).
|
||||
apply ST_Plus2.
|
||||
assumption.
|
||||
|
||||
assumption.
|
||||
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Theorem step_normalizing :
|
||||
normalizing step.
|
||||
Proof.
|
||||
unfold normalizing.
|
||||
tm_cases (induction t) Case.
|
||||
Case "tm_const".
|
||||
exists (tm_const n).
|
||||
split.
|
||||
SCase "l". apply rsc_refl.
|
||||
SCase "r".
|
||||
(* We can use rewrite with "iff" statements, not
|
||||
just equalities: *)
|
||||
rewrite nf_same_as_value. apply v_const.
|
||||
Case "tm_plus".
|
||||
destruct IHt1 as [t1' H1]. destruct IHt2 as [t2' H2].
|
||||
destruct H1 as [H11 H12]. destruct H2 as [H21 H22].
|
||||
rewrite nf_same_as_value in H12. rewrite nf_same_as_value in H22.
|
||||
inversion H12 as [n1]. inversion H22 as [n2].
|
||||
rewrite <- H in H11.
|
||||
rewrite <- H0 in H21.
|
||||
exists (tm_const (plus n1 n2)).
|
||||
split.
|
||||
SCase "l".
|
||||
apply rsc_trans with (tm_plus (tm_const n1) t2).
|
||||
apply stepmany_congr_1. apply H11.
|
||||
apply rsc_trans with
|
||||
(tm_plus (tm_const n1) (tm_const n2)).
|
||||
apply stepmany_congr2. apply v_const. apply H21.
|
||||
apply rsc_R. apply ST_PlusConstConst.
|
||||
SCase "r".
|
||||
rewrite nf_same_as_value. apply v_const. Qed.
|
||||
|
||||
Lemma eval__value : forall t1 t2,
|
||||
eval t1 t2 ->
|
||||
value t2.
|
||||
Proof.
|
||||
intros t1 t2 HE.
|
||||
eval_cases (inversion HE) Case; apply v_const. Qed.
|
||||
|
||||
|
||||
(*
|
||||
Theorem eval__stepmany: forall t v,
|
||||
eval t v -> t ===>* v.
|
||||
Proof.
|
||||
*)
|
||||
Reference in New Issue
Block a user