simpl -> cbn

1 files changed, 26 insertions, 26 deletions

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.