simpl -> cbn

1 files changed, 26 insertions, 26 deletions

diff --git a/kvx/Asmblock.v b/kvx/Asmblock.v
index 9c8e4cc3..64b2c535 100644
--- a/kvx/Asmblock.v
+++ b/kvx/Asmblock.v
@@ -78,7 +78,7 @@ Fixpoint code_to_basics (c: code) :=
 
 Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c.
 Proof.
-  intros. induction c as [|i c]; simpl; auto.
+  intros. induction c as [|i c]; cbn; auto.
   rewrite IHc. auto.
 Qed.
 
@@ -88,8 +88,8 @@ Lemma code_to_basics_dist:
   code_to_basics c' = Some l' ->
   code_to_basics (c ++ c') = Some (l ++ l').
 Proof.
-  induction c as [|i c]; simpl; auto.
-  - intros. inv H. simpl. auto.
+  induction c as [|i c]; cbn; auto.
+  - intros. inv H. cbn. auto.
   - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate.
     inv H. erewrite IHc; eauto. auto.
 Qed.
@@ -138,9 +138,9 @@ Lemma non_empty_bblock_refl:
 Proof.
   intros. split.
   - destruct body; destruct exit.
-    all: simpl; auto. intros. inversion H; contradiction.
+    all: cbn; auto. intros. inversion H; contradiction.
   - destruct body; destruct exit.
-    all: simpl; auto.
+    all: cbn; auto.
     all: intros; try (right; discriminate); try (left; discriminate).
     contradiction.
 Qed.
@@ -155,14 +155,14 @@ Lemma builtin_alone_refl:
 Proof.
   intros. split.
   - destruct body; destruct exit.
-    all: simpl; auto.
-    all: exploreInst; simpl; auto.
+    all: cbn; auto.
+    all: exploreInst; cbn; auto.
     unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto.
     assert (b :: body = nil). eapply H; eauto. discriminate.
   - destruct body; destruct exit.
-    all: simpl; auto; try constructor.
+    all: cbn; auto; try constructor.
     + exploreInst; try discriminate.
-        simpl. contradiction.
+        cbn. contradiction.
     + intros. discriminate.
 Qed.
 
@@ -185,14 +185,14 @@ Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try
 
 Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2.
 Proof.
-  destruct b; simpl; auto.
+  destruct b; cbn; auto.
   - destruct p1, p2; auto.
   - destruct p1.
 Qed.
 
 Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2.
 Proof.
-  destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl.
+  destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; cbn.
   intros; subst.
   rewrite (Istrue_proof_irrelevant _ c1 c2).
   auto.
@@ -212,51 +212,51 @@ Qed.
 Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
 Proof.
   intros. destruct l; try (contradict H; auto; fail).
-  simpl. omega.
+  cbn. omega.
 Qed.
 
 Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
 Proof.
   intros. destruct z; auto.
-  - contradict H. simpl. apply gt_irrefl.
+  - contradict H. cbn. apply gt_irrefl.
   - apply Zgt_pos_0.
-  - contradict H. simpl. apply gt_irrefl.
+  - contradict H. cbn. apply gt_irrefl.
 Qed.
 
 Lemma size_positive (b:bblock): size b > 0.
 Proof.
-  unfold size. destruct b as [hd bdy ex cor]. simpl.
-  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega).
-  inversion cor; contradict H; simpl; auto.
+  unfold size. destruct b as [hd bdy ex cor]. cbn.
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega).
+  inversion cor; contradict H; cbn; auto.
 Qed.
 
 
 Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
 Next Obligation.
-  destruct bb; simpl. assumption.
+  destruct bb; cbn. assumption.
 Defined.
 
 Lemma no_header_size:
   forall bb, size (no_header bb) = size bb.
 Proof.
-  intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity.
+  intros. destruct bb as [hd bdy ex COR]. unfold no_header. cbn. reflexivity.
 Qed.
 
 Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.
 Next Obligation.
-  destruct bb; simpl. assumption.
+  destruct bb; cbn. assumption.
 Defined.
 
 Lemma stick_header_size:
   forall h bb, size (stick_header h bb) = size bb.
 Proof.
-  intros. destruct bb. unfold stick_header. simpl. reflexivity.
+  intros. destruct bb. unfold stick_header. cbn. reflexivity.
 Qed.
 
 Lemma stick_header_no_header:
   forall bb, stick_header (header bb) (no_header bb) = bb.
 Proof.
-  intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity.
+  intros. destruct bb as [hd bdy ex COR]. cbn. unfold no_header; unfold stick_header; cbn. reflexivity.
 Qed.
 
 (** * Sequential Semantics of basic blocks *)
@@ -308,7 +308,7 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
 Theorem builtin_body_nil:
   forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
 Proof.
-  intros. destruct bb as [hd bdy ex WF]. simpl in *.
+  intros. destruct bb as [hd bdy ex WF]. cbn in *.
   apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
   eapply H1; eauto.
 Qed.
@@ -321,11 +321,11 @@ Theorem exec_body_app:
     /\ exec_body l' rs' m' = Next rs'' m''.
 Proof.
   induction l.
-  - intros. simpl in H. repeat eexists. auto.
-  - intros. rewrite <- app_comm_cons in H. simpl in H.
+  - intros. cbn in H. repeat eexists. auto.
+  - intros. rewrite <- app_comm_cons in H. cbn in H.
     destruct (exec_basic_instr a rs m) eqn:EXEBI.
     + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
-      repeat eexists. simpl. rewrite EXEBI. eauto. auto.
+      repeat eexists. cbn. rewrite EXEBI. eauto. auto.
     + discriminate.
 Qed.