Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass

4 files changed, 141 insertions, 141 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.
diff --git a/kvx/abstractbb/ImpSimuTest.v b/kvx/abstractbb/ImpSimuTest.v
index 89260ddb..b1a3b985 100644
--- a/kvx/abstractbb/ImpSimuTest.v
+++ b/kvx/abstractbb/ImpSimuTest.v
@@ -160,13 +160,13 @@ Definition list_term_set_hid (l: list_term) (hid: hashcode): list_term :=
 Lemma term_eval_set_hid ge t hid m:
   term_eval ge (term_set_hid t hid) m = term_eval ge t m.
 Proof.
-  destruct t; simpl; auto.
+  destruct t; cbn; auto.
 Qed.
 
 Lemma list_term_eval_set_hid ge l hid m:
   list_term_eval ge (list_term_set_hid l hid) m = list_term_eval ge l m.
 Proof.
-  destruct l; simpl; auto.
+  destruct l; cbn; auto.
 Qed.
 
 (* Local nickname *)
@@ -315,7 +315,7 @@ Proof.
     destruct (DM0 m) as (PRE & VALID0); clear DM0.
     assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. }
     assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, ST.term_eval ge (d x) m <> None). { unfold smem_valid in PRE; tauto. }
-    rewrite !allvalid_extensionality in * |- *; simpl.
+    rewrite !allvalid_extensionality in * |- *; cbn.
     intuition (subst; eauto).
     + eapply smem_valid_set_proof; eauto.
       erewrite <- EQT; eauto.
@@ -323,11 +323,11 @@ Proof.
       intros X1; exploit smem_valid_set_decompose_2; eauto.
       rewrite <- EQT; eauto.
     + exploit smem_valid_set_decompose_1; eauto.
-  - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl.
+  - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; cbn.
     Local Hint Resolve smem_valid_set_decompose_1: core.
     intros; case (R.eq_dec x x0).
-    + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto.
-    + intros; rewrite !Dict.set_spec_diff; simpl; eauto.
+    + intros; subst; rewrite !Dict.set_spec_eq; cbn; eauto.
+    + intros; rewrite !Dict.set_spec_diff; cbn; eauto.
 Qed.
 Local Hint Resolve naive_set_correct: core.
 
@@ -404,10 +404,10 @@ Lemma hterm_append_correct l: forall lh,
   WHEN hterm_append l lh ~> lh' THEN (forall ge m, allvalid ge lh' m <-> (allvalid ge l m /\ allvalid ge lh m)).
 Proof.
   Local Hint Resolve eq_trans: localhint.
-  induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp).
+  induction l as [|t l']; cbn; wlp_xsimplify ltac:(eauto with wlp).
   - intros; rewrite! allvalid_extensionality; intuition eauto.
   - intros REC ge m; rewrite REC; clear IHl' REC. rewrite !allvalid_extensionality.
-    simpl; intuition (subst; eauto with wlp localhint).
+    cbn; intuition (subst; eauto with wlp localhint).
 Qed.
 (*Local Hint Resolve hterm_append_correct: wlp.*)
 Global Opaque hterm_append.
@@ -431,8 +431,8 @@ Lemma smart_set_correct hd x ht:
     forall ge m y, hsmem_post_eval ge d y m = hsmem_post_eval ge (Dict.set hd x ht) y m.
 Proof.
   destruct ht; wlp_simplify.
-  unfold hsmem_post_eval; simpl. case (R.eq_dec x0 y).
-  - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. simpl; congruence.
+  unfold hsmem_post_eval; cbn. case (R.eq_dec x0 y).
+  - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. cbn; congruence.
   - intros; rewrite Dict.set_spec_diff, Dict.rem_spec_diff; auto.
 Qed.
 (*Local Hint Resolve smart_set_correct: wlp.*)
@@ -456,17 +456,17 @@ Proof.
   generalize (hterm_append_correct _ _ _ Hexta0); intro APPEND.
   generalize (hterm_lift_correct _ _ Hexta1); intro LIFT.
   generalize (smart_set_correct _ _ _ _ Hexta3); intro SMART.
-  eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; simpl. 
+  eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; cbn. 
   destruct H as (VALID & EFFECT); split.
   - intros; rewrite APPEND, <- VALID.
-    rewrite !allvalid_extensionality in * |- *; simpl; intuition (subst; eauto).
+    rewrite !allvalid_extensionality in * |- *; cbn; intuition (subst; eauto).
   - intros m x0 ALLVALID; rewrite SMART.
     destruct (term_eval ge ht m) eqn: Hht.
     * case (R.eq_dec x x0).
-      + intros; subst. unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_eq.
+      + intros; subst. unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_eq.
         erewrite LIFT, EFFECT; eauto.
-      + intros; unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_diff; auto.
-    * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto.
+      + intros; unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_diff; auto.
+    * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); cbn; auto.
 Qed.
 Local Hint Resolve hsmem_set_correct: wlp.
 Global Opaque hsmem_set.
@@ -481,7 +481,7 @@ Proof.
   intro H.
   induction e using exp_mut with (P0:=fun le =>  forall d hd,
      smem_model ge d hd -> forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge (list_exp_term le hd hod) m = list_term_eval ge (list_exp_term le d od) m); 
-     unfold smem_model in * |- * ; simpl; intuition eauto.
+     unfold smem_model in * |- * ; cbn; intuition eauto.
   - erewrite IHe; eauto.
   - erewrite IHe0, IHe; eauto.
 Qed.
@@ -516,10 +516,10 @@ Lemma exp_hterm_correct_x ge e hod od:
    induction e using exp_mut with (P0:=fun le =>  forall d hd,
      smem_model ge d hd ->
      WHEN list_exp_hterm le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = ST.list_term_eval ge (list_exp_term le d od) m); 
-     unfold smem_model, hsmem_post_eval in * |- * ; simpl; wlp_simplify.
+     unfold smem_model, hsmem_post_eval in * |- * ; cbn; wlp_simplify.
   - rewrite H1, <- H4; auto.
-  - rewrite H4, <- H0; simpl; auto.
-  - rewrite H5, <- H0, <- H4; simpl; auto.
+  - rewrite H4, <- H0; cbn; auto.
+  - rewrite H5, <- H0, <- H4; cbn; auto.
 Qed.
 Global Opaque exp_hterm.
 
@@ -544,7 +544,7 @@ Lemma hinst_smem_correct i: forall hd hod,
     forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'.
 Proof.
   Local Hint Resolve smem_valid_set_proof: core.
-  induction i; simpl; wlp_simplify; eauto 15 with wlp.
+  induction i; cbn; wlp_simplify; eauto 15 with wlp.
 Qed.
 Global Opaque hinst_smem.
 Local Hint Resolve hinst_smem_correct: wlp.
@@ -564,7 +564,7 @@ Fixpoint bblock_hsmem_rec (p: bblock) (d: hsmem): ?? hsmem :=
 Lemma bblock_hsmem_rec_correct p: forall hd,
   WHEN bblock_hsmem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'.
 Proof.
-  induction p; simpl; wlp_simplify.
+  induction p; cbn; wlp_simplify.
 Qed.
 Global Opaque bblock_hsmem_rec.
 Local Hint Resolve bblock_hsmem_rec_correct: wlp.
@@ -573,8 +573,8 @@ Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}.
 
 Lemma hsmem_empty_correct ge: smem_model ge smem_empty hsmem_empty.
 Proof.
-  unfold smem_model, smem_valid, hsmem_post_eval; simpl; intuition try congruence.
-  rewrite !Dict.empty_spec; simpl; auto.
+  unfold smem_model, smem_valid, hsmem_post_eval; cbn; intuition try congruence.
+  rewrite !Dict.empty_spec; cbn; auto.
 Qed.
 
 Definition bblock_hsmem: bblock -> ?? hsmem
@@ -722,7 +722,7 @@ Theorem g_bblock_simu_test_correct p1 p2:
   WHEN g_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
 Proof.
   wlp_simplify.
-  destruct exta0; simpl in * |- *; auto.
+  destruct exta0; cbn in * |- *; auto.
 Qed.
 Global Opaque g_bblock_simu_test.
 
@@ -1209,8 +1209,8 @@ Lemma eq_test_correct A d1: forall (d2: t A),
  WHEN eq_test d1 d2 ~> b THEN
   b=true -> forall x, get d1 x = get d2 x.
 Proof.
-  unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; simpl; 
-  wlp_simplify; (discriminate || (subst; destruct x; simpl; auto)).
+  unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; cbn; 
+  wlp_simplify; (discriminate || (subst; destruct x; cbn; auto)).
 Qed.
 Global Opaque eq_test.
 
diff --git a/kvx/abstractbb/Parallelizability.v b/kvx/abstractbb/Parallelizability.v
index 79ec9038..e5d21434 100644
--- a/kvx/abstractbb/Parallelizability.v
+++ b/kvx/abstractbb/Parallelizability.v
@@ -50,8 +50,8 @@ Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem :=
 Lemma inst_run_prun i: forall m old,
   inst_run ge i m old = inst_prun i m m old.
 Proof.
-  induction i as [|[y e] i']; simpl; auto.
-  intros m old; destruct (exp_eval ge e m old); simpl; auto.
+  induction i as [|[y e] i']; cbn; auto.
+  intros m old; destruct (exp_eval ge e m old); cbn; auto.
 Qed.
 
 
@@ -76,8 +76,8 @@ Lemma inst_prun_equiv i old: forall m1 m2 tmp,
   (forall x, m1 x = m2 x) ->
   res_eq (inst_prun i m1 tmp old) (inst_prun i m2 tmp old).
 Proof.
-  induction i as [|[x e] i']; simpl; eauto.
-  intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); simpl; auto.
+  induction i as [|[x e] i']; cbn; eauto.
+  intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); cbn; auto.
   eapply IHi'; unfold assign. intros; destruct (R.eq_dec x x0); auto.
 Qed.
 
@@ -85,12 +85,12 @@ Lemma prun_iw_equiv p: forall m1 m2 old,
   (forall x, m1 x = m2 x) ->
   res_eq (prun_iw p m1 old) (prun_iw p m2 old).
 Proof.
-  induction p as [|i p']; simpl; eauto.
+  induction p as [|i p']; cbn; eauto.
   - intros m1 m2 old H.
     generalize (inst_prun_equiv i old m1 m2 old H);
-    destruct (inst_prun i m1 old old); simpl.
-    + intros (m3 & H3 & H4); rewrite H3; simpl; eauto.
-    + intros H1; rewrite H1; simpl; auto.
+    destruct (inst_prun i m1 old old); cbn.
+    + intros (m3 & H3 & H4); rewrite H3; cbn; eauto.
+    + intros H1; rewrite H1; cbn; auto.
 Qed.
 
 
@@ -101,8 +101,8 @@ Lemma prun_iw_app p1: forall m1 old p2,
      | None => None
      end.
 Proof.
-   induction p1; simpl; try congruence.
-   intros; destruct (inst_prun _ _ _); simpl; auto.
+   induction p1; cbn; try congruence.
+   intros; destruct (inst_prun _ _ _); cbn; auto.
 Qed.
 
 Lemma prun_iw_app_None p1: forall m1 old p2,
@@ -132,12 +132,12 @@ Fixpoint notIn {A} (x: A) (l:list A): Prop :=
 
 Lemma notIn_iff A (x:A) l: (~List.In x l) <-> notIn x l.
 Proof.
-  induction l; simpl; intuition.
+  induction l; cbn; intuition.
 Qed.
 
 Lemma notIn_app A (x:A) l1: forall l2, notIn x (l1++l2) <-> (notIn x l1 /\ notIn x l2).
 Proof.
-  induction l1; simpl.
+  induction l1; cbn.
   - intuition.
   - intros; rewrite IHl1. intuition.
 Qed.
@@ -145,7 +145,7 @@ Qed.
 
 Lemma In_Permutation A (l1 l2: list A): Permutation l1 l2 -> forall x, In x l1 -> In x l2.
 Proof.
-  induction 1; simpl; intuition.
+  induction 1; cbn; intuition.
 Qed.
 
 Lemma Permutation_incl A (l1 l2: list A): Permutation l1 l2 -> incl l1 l2.
@@ -174,7 +174,7 @@ Qed.
 
 Lemma disjoint_cons_l A (x:A) (l1 l2: list A): disjoint (x::l1) l2 <-> (notIn x l2) /\ (disjoint l1 l2).
 Proof.
-  unfold disjoint. simpl; intuition subst; auto. 
+  unfold disjoint. cbn; intuition subst; auto. 
 Qed.
 
 Lemma disjoint_cons_r A (x:A) (l1 l2: list A): disjoint l1 (x::l2) <-> (notIn x l1) /\ (disjoint l1 l2).
@@ -230,13 +230,13 @@ Fixpoint frame_assign m1 (f: list R.t) m2 :=
 Lemma frame_assign_def f: forall m1 m2 x,
    frame_assign m1 f m2 x = if notIn_dec x f then m1 x else m2 x.
 Proof.
-  induction f as [|y f] ; simpl; auto.
-  - intros; destruct (notIn_dec x []); simpl in *; tauto.
-  - intros; rewrite IHf; destruct (notIn_dec x (y::f)); simpl in *.
-    + destruct (notIn_dec x f); simpl in *; intuition.
+  induction f as [|y f] ; cbn; auto.
+  - intros; destruct (notIn_dec x []); cbn in *; tauto.
+  - intros; rewrite IHf; destruct (notIn_dec x (y::f)); cbn in *.
+    + destruct (notIn_dec x f); cbn in *; intuition.
       rewrite assign_diff; auto.
       rewrite <- notIn_iff in *; intuition.
-    + destruct (notIn_dec x f); simpl in *; intuition subst.
+    + destruct (notIn_dec x f); cbn in *; intuition subst.
       rewrite assign_eq; auto.
       rewrite <- notIn_iff in *; intuition.
 Qed.
@@ -266,7 +266,7 @@ Lemma frame_eq_list_split f1 (f2: R.t -> Prop) om1 om2:
  (forall m1 m2 x, om1 = Some m1 -> om2 = Some m2 -> f2 x -> notIn x f1 -> m1 x = m2 x) ->
  frame_eq f2 om1 om2.
 Proof.
-  unfold frame_eq; destruct om1 as [ m1 | ]; simpl; auto.
+  unfold frame_eq; destruct om1 as [ m1 | ]; cbn; auto.
   intros (m2 & H0 & H1); subst.
   intros H.
   eexists; intuition eauto.
@@ -280,7 +280,7 @@ Lemma frame_eq_res_eq f om1 om2:
  res_eq om1 om2.
 Proof.
   intros H H0; lapply (frame_eq_list_split f (fun _ => True) om1 om2 H); eauto.
-  clear H H0; unfold frame_eq, res_eq. destruct om1; simpl; firstorder.
+  clear H H0; unfold frame_eq, res_eq. destruct om1; cbn; firstorder.
 Qed.
 *)
 
@@ -296,9 +296,9 @@ Lemma inst_wframe_correct i m' old: forall m tmp,
   inst_prun ge i m tmp old = Some m' -> 
   forall x, notIn x (inst_wframe i) -> m' x  = m x.
 Proof.
-  induction i as [|[y e] i']; simpl.
+  induction i as [|[y e] i']; cbn.
   - intros m tmp H x H0; inversion_clear H; auto.
-  - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); simpl; try congruence.
+  - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); cbn; try congruence.
     cutrewrite (m x = assign m y v x); eauto.
     rewrite assign_diff; auto.
 Qed.
@@ -306,9 +306,9 @@ Qed.
 Lemma inst_prun_fequiv i old: forall m1 m2 tmp, 
   frame_eq (fun x => In x (inst_wframe i)) (inst_prun ge i m1 tmp old) (inst_prun ge i m2 tmp old).
 Proof.
-  induction i as [|[y e] i']; simpl.
+  induction i as [|[y e] i']; cbn.
   - intros m1 m2 tmp; eexists; intuition eauto.
-  - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); simpl; auto.
+  - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); cbn; auto.
     eapply frame_eq_list_split; eauto. clear IHi'.
     intros m1' m2' x H1 H2.
     lapply (inst_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto.
@@ -323,7 +323,7 @@ Lemma inst_prun_None i m1 m2 tmp old:
   inst_prun ge i m2 tmp old = None.
 Proof.
   intros H; generalize (inst_prun_fequiv i old m1 m2 tmp).
-  rewrite H; simpl; auto.
+  rewrite H; cbn; auto.
 Qed.
 
 Lemma inst_prun_Some i m1 m2 tmp old m1': 
@@ -331,7 +331,7 @@ Lemma inst_prun_Some i m1 m2 tmp old m1':
   res_eq (Some (frame_assign m2 (inst_wframe i) m1')) (inst_prun ge i m2 tmp old).
 Proof.
   intros H; generalize (inst_prun_fequiv i old m1 m2 tmp).
-  rewrite H; simpl.
+  rewrite H; cbn.
   intros (m2' & H1 & H2).
   eexists; intuition eauto.
   rewrite frame_assign_def.
@@ -351,7 +351,7 @@ Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_com
 Lemma bblock_wframe_Permutation p p': 
  Permutation p p' -> Permutation (bblock_wframe p)  (bblock_wframe p').
 Proof.
-  induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; simpl; auto.
+  induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; cbn; auto.
   - rewrite! app_assoc; auto.
   - eapply Permutation_trans; eauto.
 Qed.
@@ -361,11 +361,11 @@ Lemma bblock_wframe_correct p m' old: forall m,
   prun_iw p m old = Some m' -> 
   forall x, notIn x (bblock_wframe p) -> m' x = m x.
 Proof.
-  induction p as [|i p']; simpl.
+  induction p as [|i p']; cbn.
   - intros m H; inversion_clear H; auto.
   - intros m H x; rewrite notIn_app; intros (H1 & H2). 
     remember (inst_prun i m old old) as om.
-    destruct om as [m1|]; simpl.
+    destruct om as [m1|]; cbn.
     + eapply eq_trans.
       eapply IHp'; eauto.
       eapply inst_wframe_correct; eauto.
@@ -375,12 +375,12 @@ Qed.
 Lemma prun_iw_fequiv p old: forall m1 m2, 
   frame_eq (fun x => In x (bblock_wframe p)) (prun_iw p m1 old) (prun_iw p m2 old).
 Proof.
-  induction p as [|i p']; simpl.
+  induction p as [|i p']; cbn.
   - intros m1 m2; eexists; intuition eauto.
   - intros m1 m2; generalize (inst_prun_fequiv i old m1 m2 old).
     remember (inst_prun i m1 old old) as om.
-    destruct om as [m1'|]; simpl.
-    + intros (m2' & H1 & H2). rewrite H1; simpl.
+    destruct om as [m1'|]; cbn.
+    + intros (m2' & H1 & H2). rewrite H1; cbn.
     eapply frame_eq_list_split; eauto. clear IHp'.
     intros m1'' m2'' x H3 H4. rewrite in_app_iff.
     intros X X2. assert (X1: In x (inst_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. }
@@ -389,7 +389,7 @@ Proof.
     lapply (bblock_wframe_correct p' m2'' old m2'); eauto.
     intros Xm2' Xm1'. 
     rewrite Xm1', Xm2'; auto.
-    + intro H; rewrite H; simpl; auto.
+    + intro H; rewrite H; cbn; auto.
 Qed.
 
 Lemma prun_iw_equiv p m1 m2 old: 
@@ -418,7 +418,7 @@ Fixpoint is_det (p: bblock): Prop :=
 Lemma is_det_Permutation p p': 
  Permutation p p' -> is_det p -> is_det p'.
 Proof.
-  induction 1; simpl; auto.
+  induction 1; cbn; auto.
   - intros; intuition. eapply disjoint_incl_r. 2: eauto.
     eapply Permutation_incl. eapply Permutation_sym. 
     eapply bblock_wframe_Permutation; auto.
@@ -431,20 +431,20 @@ Theorem is_det_correct p p':
   is_det p -> 
   forall m old, res_eq (prun_iw ge p m old) (prun_iw ge p' m old).
 Proof.
-  induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; simpl; eauto.
+  induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; cbn; eauto.
   - intros [H0 H1] m old.
     remember (inst_prun ge i m old old) as om0.
-    destruct om0 as [ m0 | ]; simpl; auto.
+    destruct om0 as [ m0 | ]; cbn; auto.
   - rewrite disjoint_app_r.
     intros ([Z1 Z2] & Z3 & Z4) m old.
     remember (inst_prun ge i2 m old old) as om2.
-    destruct om2 as [ m2 | ]; simpl; auto.
+    destruct om2 as [ m2 | ]; cbn; auto.
     + remember (inst_prun ge i1 m old old) as om1.
-      destruct om1 as [ m1 | ]; simpl; auto.
-      * lapply (inst_prun_Some i2 m m1 old old m2); simpl; auto.
-        lapply (inst_prun_Some i1 m m2 old old m1); simpl; auto.
+      destruct om1 as [ m1 | ]; cbn; auto.
+      * lapply (inst_prun_Some i2 m m1 old old m2); cbn; auto.
+        lapply (inst_prun_Some i1 m m2 old old m1); cbn; auto.
         intros (m1' & Hm1' & Xm1') (m2' & Hm2' & Xm2').
-        rewrite Hm1', Hm2'; simpl.
+        rewrite Hm1', Hm2'; cbn.
         eapply prun_iw_equiv.
         intros x; rewrite <- Xm1', <- Xm2'. clear Xm2' Xm1' Hm1' Hm2' m1' m2'.
         rewrite frame_assign_def.
@@ -455,9 +455,9 @@ Proof.
           erewrite (inst_wframe_correct i1 m1 old m old); eauto.
         }
         rewrite frame_assign_notIn; auto.
-     * erewrite inst_prun_None; eauto. simpl; auto.
+     * erewrite inst_prun_None; eauto. cbn; auto.
    + remember (inst_prun ge i1 m old old) as om1.
-     destruct om1 as [ m1 | ]; simpl; auto.
+     destruct om1 as [ m1 | ]; cbn; auto.
      erewrite inst_prun_None; eauto.
   - intros; eapply res_eq_trans.
     eapply IHPermutation1; eauto.
@@ -486,7 +486,7 @@ Lemma exp_frame_correct e old1 old2:
    (exp_eval ge e m1 old1)=(exp_eval ge e m2 old2).
 Proof.
   induction e using exp_mut with (P0:=fun l => (forall x, In x (list_exp_frame l) -> old1 x = old2 x) -> forall m1 m2, (forall x, In x (list_exp_frame l) -> m1 x = m2 x) ->
-   (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); simpl; auto.
+   (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); cbn; auto.
   - intros H1 m1 m2 H2; rewrite H2; auto.
   - intros H1 m1 m2 H2; erewrite IHe; eauto.
   - intros H1 m1 m2 H2; erewrite IHe, IHe0; eauto; 
@@ -501,7 +501,7 @@ Fixpoint inst_frame (i: inst): list R.t :=
 
 Lemma inst_wframe_frame i x: In x (inst_wframe i) -> In x (inst_frame i).
 Proof.
-  induction i as [ | [y e] i']; simpl; intuition.
+  induction i as [ | [y e] i']; cbn; intuition.
 Qed.
 
 
@@ -511,13 +511,13 @@ Lemma inst_frame_correct i wframe old1 old2: forall m tmp1 tmp2,
   (forall x, notIn x wframe -> tmp1 x = tmp2 x) ->
   inst_prun ge i m tmp1 old1 = inst_prun ge i m tmp2 old2.
 Proof.
-  induction i as [|[x e] i']; simpl; auto.
+  induction i as [|[x e] i']; cbn; auto.
   intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l.
   intros (H1 & H2 & H3) H6 H7.
   cutrewrite (exp_eval ge e tmp1 old1 = exp_eval ge e tmp2 old2).
   - destruct (exp_eval ge e tmp2 old2); auto.
     eapply IHi'; eauto. 
-    simpl; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); simpl; auto. 
+    cbn; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); cbn; auto. 
   - unfold disjoint in H2; apply exp_frame_correct.
     intros;apply H6; auto.
     intros;apply H7; auto.
@@ -535,8 +535,8 @@ Fixpoint pararec (p: bblock) (wframe: list R.t): Prop :=
 
 Lemma pararec_disjoint (p: bblock): forall wframe, pararec p wframe -> disjoint (bblock_wframe p) wframe.
 Proof.
-  induction p as [|i p']; simpl.
-  - unfold disjoint; simpl; intuition.
+  induction p as [|i p']; cbn.
+  - unfold disjoint; cbn; intuition.
   - intros wframe [H0 H1]; rewrite disjoint_app_l. 
     generalize (IHp' _ H1).
     rewrite disjoint_app_r. intuition. 
@@ -546,7 +546,7 @@ Qed.
 
 Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p.
 Proof.
-  induction p as [|i p']; simpl; auto.
+  induction p as [|i p']; cbn; auto.
   intros wframe [H0 H1]. generalize (pararec_disjoint _ _ H1). rewrite disjoint_app_r.
   intuition. 
   - apply disjoint_sym; auto.
@@ -558,7 +558,7 @@ Lemma pararec_correct p old: forall wframe m,
   (forall x, notIn x wframe -> m x = old x) ->
   run ge p m = prun_iw ge p m old.
 Proof.
-  elim p; clear p; simpl; auto.
+  elim p; clear p; cbn; auto.
   intros i p' X wframe m [H H0] H1.
   erewrite inst_run_prun, inst_frame_correct; eauto.
   remember (inst_prun ge i m old old) as om0.
@@ -646,7 +646,7 @@ Fixpoint inst_wsframe(i:inst): S.t :=
 
 Lemma inst_wsframe_correct i: S.match_frame (inst_wsframe i) (inst_wframe i).
 Proof.
-  induction i; simpl; auto.
+  induction i; cbn; auto.
 Qed.
 
 Fixpoint exp_sframe (e: exp): S.t :=
@@ -664,7 +664,7 @@ with list_exp_sframe (le: list_exp): S.t :=
 
 Lemma exp_sframe_correct e: S.match_frame (exp_sframe e) (exp_frame e).
 Proof.
-  induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); simpl; auto.
+  induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); cbn; auto.
 Qed.
 
 Fixpoint inst_sframe (i: inst): S.t :=
@@ -677,7 +677,7 @@ Local Hint Resolve exp_sframe_correct: core.
 
 Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i).
 Proof.
-  induction i as [|[y e] i']; simpl; auto.
+  induction i as [|[y e] i']; cbn; auto.
 Qed.
 
 Local Hint Resolve inst_wsframe_correct inst_sframe_correct: core.
@@ -692,7 +692,7 @@ Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool :=
 
 Lemma is_pararec_correct (p: bblock): forall s l, S.match_frame s l -> (is_pararec p s)=true -> (pararec p l).
 Proof.
-  induction p; simpl; auto.
+  induction p; cbn; auto.
   intros s l H1 H2; rewrite lazy_andb_bool_true in H2. destruct H2 as [H2 H3].
   constructor 1; eauto.
 Qed.
@@ -739,14 +739,14 @@ Definition empty:=PositiveSet.empty.
 
 Lemma empty_match_frame: match_frame empty nil.
 Proof.
-  unfold match_frame, empty, PositiveSet.In; simpl; intuition.
+  unfold match_frame, empty, PositiveSet.In; cbn; intuition.
 Qed.
 
 Definition add: R.t -> t -> t := PositiveSet.add.
 
 Lemma add_match_frame: forall s x l, match_frame s l -> match_frame (add x s) (x::l).
 Proof.
-  unfold match_frame, add; simpl. 
+  unfold match_frame, add; cbn. 
   intros s x l H y. rewrite PositiveSet.add_spec, H.
   intuition. 
 Qed.
@@ -772,13 +772,13 @@ Fixpoint is_disjoint (s s': PositiveSet.t) : bool :=
 
 Lemma is_disjoint_spec_true s: forall s', is_disjoint s s' = true -> forall x, PositiveSet.In x s -> PositiveSet.In x s' -> False.
 Proof.
-  unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; simpl; try discriminate.
-  destruct s' as [|l' o' r']; simpl; try discriminate.
+  unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; cbn; try discriminate.
+  destruct s' as [|l' o' r']; cbn; try discriminate.
   intros X.
   assert (H: ~(o = true /\ o'=true) /\ is_disjoint l l' = true /\ is_disjoint r r'=true).
-  { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); simpl in X; intuition. }
+  { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); cbn in X; intuition. }
   clear X; destruct H as (H & H1 & H2).
-  destruct x as [i|i|]; simpl; eauto.
+  destruct x as [i|i|]; cbn; eauto.
 Qed.
 
 Lemma is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2.
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.