simpl -> cbn

1 files changed, 25 insertions, 25 deletions

diff --git a/kvx/abstractbb/AbstractBasicBlocksDef.v b/kvx/abstractbb/AbstractBasicBlocksDef.v
index 948ed660..6960f363 100644
--- a/kvx/abstractbb/AbstractBasicBlocksDef.v
+++ b/kvx/abstractbb/AbstractBasicBlocksDef.v
@@ -170,7 +170,7 @@ Lemma exp_equiv e old1 old2:
    (exp_eval e m1 old1) = (exp_eval e m2 old2).
 Proof.
   intros H1.
-  induction e using exp_mut with (P0:=fun l =>  forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); simpl; try congruence; auto.
+  induction e using exp_mut with (P0:=fun l =>  forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); cbn; try congruence; auto.
   - intros; erewrite IHe; eauto.
   - intros; erewrite IHe, IHe0; auto.
 Qed.
@@ -183,38 +183,38 @@ Lemma inst_equiv_refl i old1 old2:
   forall m1 m2, (forall x, m1 x = m2 x) -> 
   res_eq (inst_run i m1 old1) (inst_run i m2 old2).
 Proof.
-  intro H; induction i as [ | [x e]]; simpl; eauto.
+  intro H; induction i as [ | [x e]]; cbn; eauto.
   intros m1 m2 H1. erewrite exp_equiv; eauto.
-  destruct (exp_eval e m2 old2); simpl; auto.
+  destruct (exp_eval e m2 old2); cbn; auto.
   apply IHi.
   unfold assign; intro y. destruct (R.eq_dec x y); auto. 
 Qed.
 
 Lemma bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2).
 Proof.
-  induction p as [ | i p']; simpl; eauto.
+  induction p as [ | i p']; cbn; eauto.
   intros m1 m2 H; lapply (inst_equiv_refl i m1 m2); auto.
   intros X; lapply (X m1 m2); auto; clear X.
-  destruct (inst_run i m1 m1); simpl.
-  - intros [m3 [H1 H2]]; rewrite H1; simpl; auto.
-  - intros H1; rewrite H1; simpl; auto.
+  destruct (inst_run i m1 m1); cbn.
+  - intros [m3 [H1 H2]]; rewrite H1; cbn; auto.
+  - intros H1; rewrite H1; cbn; auto.
 Qed.
 
 Lemma res_eq_sym om1 om2: res_eq om1 om2 -> res_eq om2 om1.
 Proof.
-  destruct om1; simpl.
-  - intros [m2 [H1 H2]]; subst; simpl. eauto.
-  - intros; subst; simpl; eauto.
+  destruct om1; cbn.
+  - intros [m2 [H1 H2]]; subst; cbn. eauto.
+  - intros; subst; cbn; eauto.
 Qed.
 
 Lemma res_eq_trans (om1 om2 om3: option mem): 
   (res_eq om1 om2) -> (res_eq om2 om3) -> (res_eq om1 om3).
 Proof.
-  destruct om1; simpl.
-  - intros [m2 [H1 H2]]; subst; simpl.
-    intros [m3 [H3 H4]]; subst; simpl.
+  destruct om1; cbn.
+  - intros [m2 [H1 H2]]; subst; cbn.
+    intros [m3 [H3 H4]]; subst; cbn.
     eapply ex_intro; intuition eauto. rewrite H2; auto.
-  - intro; subst; simpl; auto.
+  - intro; subst; cbn; auto.
 Qed.
 
 Lemma bblock_simu_alt p1 p2: bblock_simu p1 p2 <-> (forall m1 m2,  (forall x, m1 x = m2 x) -> (run p1 m1)<>None -> res_eq (run p1 m1) (run p2 m2)).
@@ -232,8 +232,8 @@ Lemma run_app p1: forall m1 p2,
      | None => None
      end.
 Proof.
-   induction p1; simpl; try congruence.
-   intros; destruct (inst_run _ _ _); simpl; auto.
+   induction p1; cbn; try congruence.
+   intros; destruct (inst_run _ _ _); cbn; auto.
 Qed.
 
 Lemma run_app_None p1 m1 p2:
@@ -334,7 +334,7 @@ Fixpoint allvalid ge (l: list term) m : Prop :=
 Lemma allvalid_extensionality ge (l: list term) m:
   allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None).
 Proof.
-  induction l as [|t l]; simpl; try (tauto).
+  induction l as [|t l]; cbn; try (tauto).
   destruct l.
   - intuition (congruence || eauto).
   - rewrite IHl; clear IHl. intuition (congruence || eauto).
@@ -365,7 +365,7 @@ Qed.
 Lemma intro_fail_correct (l: list term) (t: term) :
    (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t).
 Proof.
-  unfold match_pt; simpl; intros; intuition congruence.
+  unfold match_pt; cbn; intros; intuition congruence.
 Qed.
 Hint Resolve intro_fail_correct: wlp.
 
@@ -374,7 +374,7 @@ Definition identity_fail (t: term):= intro_fail [t] t.
 
 Lemma identity_fail_correct (t: term): match_pt t (identity_fail t).
 Proof.
-  eapply intro_fail_correct; simpl; tauto.
+  eapply intro_fail_correct; cbn; tauto.
 Qed.
 Global Opaque identity_fail.
 Hint Resolve identity_fail_correct: wlp.
@@ -390,11 +390,11 @@ Definition nofail (is_constant: op -> bool) (t: term):=
 Lemma nofail_correct (is_constant: op -> bool) t:
  (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t).
 Proof.
-  destruct t; simpl.
-  + intros; eapply intro_fail_correct; simpl; intuition congruence.
-  + intros; destruct l; simpl; auto with wlp.
-    destruct (is_constant o) eqn:Heqo; simpl; intuition eauto with wlp.
-     eapply intro_fail_correct; simpl; intuition eauto with wlp.
+  destruct t; cbn.
+  + intros; eapply intro_fail_correct; cbn; intuition congruence.
+  + intros; destruct l; cbn; auto with wlp.
+    destruct (is_constant o) eqn:Heqo; cbn; intuition eauto with wlp.
+     eapply intro_fail_correct; cbn; intuition eauto with wlp.
 Qed.
 Global Opaque nofail.
 Hint Resolve nofail_correct: wlp.
@@ -425,7 +425,7 @@ Lemma app_fail_allvalid_correct l pt t1 t2: forall
   (V2: forall (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail {| mayfail := t1 :: l; effect := t1 |}) m)
   (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail (app_fail l pt)) m.
 Proof.
-  intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; simpl. clear V1 V2.
+  intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; cbn. clear V1 V2.
   intuition subst.
   + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto.
   + eapply H3; eauto.