diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-29 16:22:18 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-29 17:08:56 +0200 |
commit | b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 (patch) | |
tree | b6e835836c78566162d79c83bf353aa555a1d95c /kvx/abstractbb/SeqSimuTheory.v | |
parent | 52b4f973646c3b79804fcdddeed5325ab1f3ce7d (diff) | |
download | compcert-kvx-b2fc9b55d9c59a9c507786a650377e2f0a1ddad8.tar.gz compcert-kvx-b2fc9b55d9c59a9c507786a650377e2f0a1ddad8.zip |
simpl -> cbn
Diffstat (limited to 'kvx/abstractbb/SeqSimuTheory.v')
-rw-r--r-- | kvx/abstractbb/SeqSimuTheory.v | 56 |
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. |