aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/abstractbb/SeqSimuTheory.v
diff options
context:
space:
mode:
Diffstat (limited to 'kvx/abstractbb/SeqSimuTheory.v')
-rw-r--r--kvx/abstractbb/SeqSimuTheory.v56
1 files changed, 28 insertions, 28 deletions
diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v
index a957c50a..df6b9963 100644
--- a/kvx/abstractbb/SeqSimuTheory.v
+++ b/kvx/abstractbb/SeqSimuTheory.v
@@ -92,13 +92,13 @@ Variable ge: genv.
Lemma set_spec_eq d x t m:
term_eval ge (smem_set d x t x) m = term_eval ge t m.
Proof.
- unfold smem_set; simpl; case (R.eq_dec x x); try congruence.
+ unfold smem_set; cbn; case (R.eq_dec x x); try congruence.
Qed.
Lemma set_spec_diff d x y t m:
x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m.
Proof.
- unfold smem_set; simpl; case (R.eq_dec x y); try congruence.
+ unfold smem_set; cbn; case (R.eq_dec x y); try congruence.
Qed.
Fixpoint inst_smem (i: inst) (d old: smem): smem :=
@@ -123,15 +123,15 @@ Definition bblock_smem: bblock -> smem
Lemma inst_smem_pre_monotonic i old: forall d m,
(pre (inst_smem i d old) ge m) -> (pre d ge m).
Proof.
- induction i as [|[y e] i IHi]; simpl; auto.
+ induction i as [|[y e] i IHi]; cbn; auto.
intros d a H; generalize (IHi _ _ H); clear H IHi.
- unfold smem_set; simpl; intuition.
+ unfold smem_set; cbn; intuition.
Qed.
Lemma bblock_smem_pre_monotonic p: forall d m,
(pre (bblock_smem_rec p d) ge m) -> (pre d ge m).
Proof.
- induction p as [|i p' IHp']; simpl; eauto.
+ induction p as [|i p' IHp']; cbn; eauto.
intros d a H; eapply inst_smem_pre_monotonic; eauto.
Qed.
@@ -146,7 +146,7 @@ Proof.
intro H.
induction e using exp_mut with
(P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old);
- simpl; auto.
+ cbn; auto.
- intros; erewrite IHe; eauto.
- intros. erewrite IHe, IHe0; eauto.
Qed.
@@ -156,12 +156,12 @@ Lemma inst_smem_abort i m0 x old: forall (d:smem),
term_eval ge (d x) m0 = None ->
term_eval ge (inst_smem i d old x) m0 = None.
Proof.
- induction i as [|[y e] i IHi]; simpl; auto.
+ induction i as [|[y e] i IHi]; cbn; auto.
intros d VALID H; erewrite IHi; eauto. clear IHi.
- unfold smem_set; simpl; destruct (R.eq_dec y x); auto.
+ unfold smem_set; cbn; destruct (R.eq_dec y x); auto.
subst;
generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID.
- unfold smem_set; simpl. intuition congruence.
+ unfold smem_set; cbn. intuition congruence.
Qed.
Lemma block_smem_rec_abort p m0 x: forall d,
@@ -169,7 +169,7 @@ Lemma block_smem_rec_abort p m0 x: forall d,
term_eval ge (d x) m0 = None ->
term_eval ge (bblock_smem_rec p d x) m0 = None.
Proof.
- induction p; simpl; auto.
+ induction p; cbn; auto.
intros d VALID H; erewrite IHp; eauto. clear IHp.
eapply inst_smem_abort; eauto.
Qed.
@@ -181,13 +181,13 @@ Lemma inst_smem_Some_correct1 i m0 old (od:smem):
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
forall x, term_eval ge (inst_smem i d od x) m0 = Some (m2 x).
Proof.
- intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H.
+ intro X; induction i as [|[x e] i IHi]; cbn; intros m1 m2 d H.
- inversion_clear H; eauto.
- intros H0 x0.
destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence.
refine (IHi _ _ _ _ _ _); eauto.
clear x0; intros x0.
- unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto.
+ unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto.
subst; erewrite term_eval_exp; eauto.
Qed.
@@ -197,7 +197,7 @@ Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem),
forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x).
Proof.
Local Hint Resolve inst_smem_Some_correct1: core.
- induction p as [ | i p]; simpl; intros m1 m2 d H.
+ induction p as [ | i p]; cbn; intros m1 m2 d H.
- inversion_clear H; eauto.
- intros H0 x0.
destruct (inst_run ge i m1 m1) eqn: Heqov.
@@ -218,15 +218,15 @@ Lemma inst_smem_None_correct i m0 old (od: smem):
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
inst_run ge i m1 old = None -> exists x, term_eval ge (inst_smem i d od x) m0 = None.
Proof.
- intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d.
+ intro X; induction i as [|[x e] i IHi]; cbn; intros m1 d.
- discriminate.
- intros VALID H0.
destruct (exp_eval ge e m1 old) eqn: Heqov.
+ refine (IHi _ _ _ _); eauto.
- intros x0; unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto.
+ intros x0; unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto.
subst; erewrite term_eval_exp; eauto.
+ intuition.
- constructor 1 with (x:=x); simpl.
+ constructor 1 with (x:=x); cbn.
apply inst_smem_abort; auto.
rewrite set_spec_eq.
erewrite term_eval_exp; eauto.
@@ -241,14 +241,14 @@ Lemma inst_smem_Some_correct2 i m0 old (od: smem):
res_eq (Some m2) (inst_run ge i m1 old).
Proof.
intro X.
- induction i as [|[x e] i IHi]; simpl; intros m1 m2 d VALID H0.
+ induction i as [|[x e] i IHi]; cbn; intros m1 m2 d VALID H0.
- intros H; eapply ex_intro; intuition eauto.
generalize (H0 x); rewrite H.
congruence.
- intros H.
destruct (exp_eval ge e m1 old) eqn: Heqov.
+ refine (IHi _ _ _ _ _ _); eauto.
- intros x0; unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto.
+ intros x0; unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto.
subst; erewrite term_eval_exp; eauto.
+ generalize (H x).
rewrite inst_smem_abort; discriminate || auto.
@@ -262,7 +262,7 @@ Lemma bblocks_smem_rec_Some_correct2 p m0: forall (m1 m2: mem) d,
(forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x)) ->
res_eq (Some m2) (run ge p m1).
Proof.
- induction p as [|i p]; simpl; intros m1 m2 d VALID H0.
+ induction p as [|i p]; cbn; intros m1 m2 d VALID H0.
- intros H; eapply ex_intro; intuition eauto.
generalize (H0 x); rewrite H.
congruence.
@@ -293,13 +293,13 @@ Lemma inst_valid i m0 old (od:smem):
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
pre (inst_smem i d od) ge m0.
Proof.
- induction i as [|[x e] i IHi]; simpl; auto.
+ induction i as [|[x e] i IHi]; cbn; auto.
intros Hold m1 m2 d VALID0 H Hm1.
- destruct (exp_eval ge e m1 old) eqn: Heq; simpl; try congruence.
+ destruct (exp_eval ge e m1 old) eqn: Heq; cbn; try congruence.
eapply IHi; eauto.
- + unfold smem_set in * |- *; simpl.
+ + unfold smem_set in * |- *; cbn.
rewrite Hm1; intuition congruence.
- + intros x0. unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto.
+ + intros x0. unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto.
subst; erewrite term_eval_exp; eauto.
Qed.
@@ -311,7 +311,7 @@ Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem),
pre (bblock_smem_rec p d) ge m0.
Proof.
Local Hint Resolve inst_valid: core.
- induction p as [ | i p]; simpl; intros m1 d H; auto.
+ induction p as [ | i p]; cbn; intros m1 d H; auto.
intros H0 H1.
destruct (inst_run ge i m1 m1) eqn: Heqov; eauto.
congruence.
@@ -322,7 +322,7 @@ Lemma bblock_smem_valid p m0 m1:
pre (bblock_smem p) ge m0.
Proof.
intros; eapply block_smem_rec_valid; eauto.
- unfold smem_empty; simpl. auto.
+ unfold smem_empty; cbn. auto.
Qed.
Definition smem_valid ge d m := pre d ge m /\ forall x, term_eval ge (d x) m <> None.
@@ -339,7 +339,7 @@ Theorem bblock_smem_simu p1 p2:
Proof.
Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core.
intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-.
- destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence.
+ destruct (run ge p1 m) as [m1|] eqn: RUN1; cbn; try congruence.
assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto.
eapply bblock_smem_Some_correct2; eauto.
+ destruct (INCL m); intuition eauto.
@@ -371,7 +371,7 @@ Lemma smem_valid_set_proof d x t m:
Proof.
unfold smem_valid; intros (PRE & VALID) PREt. split.
+ split; auto.
- + intros x0; unfold smem_set; simpl; case (R.eq_dec x x0); intros; subst; auto.
+ + intros x0; unfold smem_set; cbn; case (R.eq_dec x x0); intros; subst; auto.
Qed.
@@ -384,7 +384,7 @@ Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:=
Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m).
Proof.
- unfold smem_correct; simpl; intros m'; split.
+ unfold smem_correct; cbn; intros m'; split.
+ intros; split.
* eapply bblock_smem_valid; eauto.
* eapply bblock_smem_Some_correct1; eauto.
generated by cgit (git 2.34.1) at 2024-07-12 05:12:42 +0000