simpl -> cbn

1 files changed, 240 insertions, 244 deletions

diff --git a/kvx/Op.v b/kvx/Op.v
index 544bb081..e2ffa3e5 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -508,9 +508,9 @@ Qed.
 Ltac FuncInv :=
   match goal with
   | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
-      destruct x; simpl in H; FuncInv
+      destruct x; cbn in H; FuncInv
   | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ =>
-      destruct v; simpl in H; FuncInv
+      destruct v; cbn in H; FuncInv
   | H: (if Archi.ptr64 then _ else _) = Some _ |- _ =>
       destruct Archi.ptr64 eqn:?; FuncInv
   | H: (Some _ = Some _) |- _ =>
@@ -727,27 +727,27 @@ Qed.
 Remark type_sub:
   forall v1 v2, Val.has_type (Val.sub v1 v2) Tint.
 Proof.
-  intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; simpl; auto.
+  intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; cbn; auto.
   destruct (eq_block _ _); auto.
 Qed.
 
 Remark type_subl:
   forall v1 v2, Val.has_type (Val.subl v1 v2) Tlong.
 Proof.
-  intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; simpl; auto.
+  intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; cbn; auto.
   destruct (eq_block _ _); auto.
 Qed.
 
 Remark type_shl:
   forall v1 v2, Val.has_type (Val.shl v1 v2) Tint.
 Proof.
-  destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial.
+  destruct v1, v2; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial.
 Qed.
 
 Remark type_shll:
   forall v1 v2, Val.has_type (Val.shll v1 v2) Tlong.
 Proof.
-  destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial.
+  destruct v1, v2; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial.
 Qed.
 
 Lemma type_of_operation_sound:
@@ -757,7 +757,7 @@ Lemma type_of_operation_sound:
   Val.has_type v (snd (type_of_operation op)).
 Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   intros.
-  destruct op; simpl; simpl in H0; FuncInv; subst; simpl.
+  destruct op; cbn; cbn in H0; FuncInv; subst; cbn.
   (* move *)
   - congruence.
   (* intconst, longconst, floatconst, singleconst *)
@@ -777,30 +777,30 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - apply type_add.
   (* addx, addximm *)
   - apply type_add.
-  - destruct v0; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
+  - destruct v0; cbn; trivial.
+    destruct (Int.ltu _ _); cbn; trivial.
   (* neg, sub *)
   - destruct v0...
   - apply type_sub.
   (* revsubimm, revsubx, revsubximm *)
   - destruct v0...
   - apply type_sub.
-  - destruct v0; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
+  - destruct v0; cbn; trivial.
+    destruct (Int.ltu _ _); cbn; trivial.
   (* mul, mulimm, mulhs, mulhu *)
   - destruct v0; destruct v1...
   - destruct v0...
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
   (* div, divu *)
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
-  - destruct v0; destruct v1; simpl in *; inv H0.
+  - destruct v0; destruct v1; cbn in *; inv H0.
+    destruct (_ || _); inv H2...
+  - destruct v0; destruct v1; cbn in *; inv H0.
     destruct (Int.eq i0 Int.zero); inv H2...
   (* mod, modu *)
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
-  - destruct v0; destruct v1; simpl in *; inv H0.
+  - destruct v0; destruct v1; cbn in *; inv H0.
+    destruct (_ || _); inv H2...
+  - destruct v0; destruct v1; cbn in *; inv H0.
     destruct (Int.eq i0 Int.zero); inv H2...
   (* and, andimm *)
   - destruct v0; destruct v1...
@@ -829,18 +829,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; destruct v1...
   - destruct v0...
   (* shl, shlimm *)
-  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
-  - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
+  - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)...
+  - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)...
   (* shr, shrimm *)
-  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
-  - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
+  - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)...
+  - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)...
   (* shru, shruimm *)
-  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
-  - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
+  - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)...
+  - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)...
   (* shrx *)
-  - destruct v0; simpl... destruct (Int.ltu n (Int.repr 31)); simpl; trivial.
+  - destruct v0; cbn... destruct (Int.ltu n (Int.repr 31)); cbn; trivial.
   (* shrimm *)
-  - destruct v0; simpl...   
+  - destruct v0; cbn...   
   (* madd *)
   - apply type_add.
   - apply type_add.
@@ -858,13 +858,13 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - apply type_addl.
   (* addxl addxlimm *)
   - apply type_addl.
-  - destruct v0; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
+  - destruct v0; cbn; trivial.
+    destruct (Int.ltu _ _); cbn; trivial.
   (* negl, subl *)
   - destruct v0...
   - apply type_subl.
-  - destruct v0; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
+  - destruct v0; cbn; trivial.
+    destruct (Int.ltu _ _); cbn; trivial.
   - destruct v0...
   - apply type_subl.
   (* mull, mullhs, mullhu *)
@@ -873,14 +873,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
   (* divl, divlu *)
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2...
-  - destruct v0; destruct v1; simpl in *; inv H0.
+  - destruct v0; destruct v1; cbn in *; inv H0.
+    destruct (_ || _); inv H2...
+  - destruct v0; destruct v1; cbn in *; inv H0.
     destruct (Int64.eq i0 Int64.zero); inv H2...
   (* modl, modlu *)
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2...
-  - destruct v0; destruct v1; simpl in *; inv H0.
+  - destruct v0; destruct v1; cbn in *; inv H0.
+    destruct (_ || _); inv H2...
+  - destruct v0; destruct v1; cbn in *; inv H0.
     destruct (Int64.eq i0 Int64.zero); inv H2...
   (* andl, andlimm *)
   - destruct v0; destruct v1...
@@ -909,16 +909,16 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; destruct v1...
   - destruct v0...
   (* shll, shllimm *)
-  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
-  - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
+  - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')...
+  - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')...
   (* shr, shrimm *)
-  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
-  - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
+  - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')...
+  - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')...
   (* shru, shruimm *)
-  - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
-  - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
+  - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')...
+  - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')...
   (* shrxl *)
-  - destruct v0; simpl... destruct (Int.ltu n (Int.repr 63)); simpl; trivial.
+  - destruct v0; cbn... destruct (Int.ltu n (Int.repr 63)); cbn; trivial.
   (* maddl, maddlim *)
   - apply type_addl.
   - apply type_addl.
@@ -960,59 +960,59 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0...
   - destruct v0...
   (* intoffloat, intuoffloat *)
-  - destruct v0; simpl... destruct (Float.to_int f); simpl; trivial.
-  - destruct v0; simpl... destruct (Float.to_intu f); simpl; trivial.
+  - destruct v0; cbn... destruct (Float.to_int f); cbn; trivial.
+  - destruct v0; cbn... destruct (Float.to_intu f); cbn; trivial.
   (* intofsingle, intuofsingle *)
-  - destruct v0; simpl...  destruct (Float32.to_int f); simpl; trivial.
-  - destruct v0; simpl...  destruct (Float32.to_intu f); simpl; trivial.
+  - destruct v0; cbn...  destruct (Float32.to_int f); cbn; trivial.
+  - destruct v0; cbn...  destruct (Float32.to_intu f); cbn; trivial.
   (* singleofint, singleofintu *)
-  - destruct v0; simpl...
-  - destruct v0; simpl...
+  - destruct v0; cbn...
+  - destruct v0; cbn...
   (* longoffloat, longuoffloat *)
-  - destruct v0; simpl... destruct (Float.to_long f); simpl; trivial.
-  - destruct v0; simpl... destruct (Float.to_longu f); simpl; trivial.
+  - destruct v0; cbn... destruct (Float.to_long f); cbn; trivial.
+  - destruct v0; cbn... destruct (Float.to_longu f); cbn; trivial.
   (* floatoflong, floatoflongu *)
-  - destruct v0; simpl...
-  - destruct v0; simpl...
+  - destruct v0; cbn...
+  - destruct v0; cbn...
   (* longofsingle, longuofsingle *)
-  - destruct v0; simpl... destruct (Float32.to_long f); simpl; trivial.
-  - destruct v0; simpl... destruct (Float32.to_longu f); simpl; trivial.
+  - destruct v0; cbn... destruct (Float32.to_long f); cbn; trivial.
+  - destruct v0; cbn... destruct (Float32.to_longu f); cbn; trivial.
   (* singleoflong, singleoflongu *)
-  - destruct v0; simpl...
-  - destruct v0; simpl...
+  - destruct v0; cbn...
+  - destruct v0; cbn...
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
  (* extfz *)
   - unfold extfz.
     destruct (is_bitfield _ _).
-    + destruct v0; simpl; trivial.
+    + destruct v0; cbn; trivial.
     + constructor.
  (* extfs *)
   - unfold extfs.
     destruct (is_bitfield _ _).
-    + destruct v0; simpl; trivial.
+    + destruct v0; cbn; trivial.
     + constructor.
  (* extfzl *)
   - unfold extfzl.
     destruct (is_bitfieldl _ _).
-    + destruct v0; simpl; trivial.
+    + destruct v0; cbn; trivial.
     + constructor.
  (* extfsl *)
   - unfold extfsl.
     destruct (is_bitfieldl _ _).
-    + destruct v0; simpl; trivial.
+    + destruct v0; cbn; trivial.
     + constructor.
  (* insf *)
   - unfold insf, bitfield_mask.
     destruct (is_bitfield _ _).
-    + destruct v0; destruct v1; simpl; trivial.
-      destruct (Int.ltu _ _); simpl; trivial.
+    + destruct v0; destruct v1; cbn; trivial.
+      destruct (Int.ltu _ _); cbn; trivial.
     + constructor.
  (* insf *)
   - unfold insfl, bitfield_mask.
     destruct (is_bitfieldl _ _).
-    + destruct v0; destruct v1; simpl; trivial.
-      destruct (Int.ltu _ _); simpl; trivial.
+    + destruct v0; destruct v1; cbn; trivial.
+      destruct (Int.ltu _ _); cbn; trivial.
     + constructor.
  (* Osel *)
   - unfold Val.select. destruct (eval_condition0 _ _ m).
@@ -1047,7 +1047,7 @@ Lemma is_trapping_op_sound:
     eval_operation genv sp op vl m <> None.
 Proof.
   unfold args_of_operation.
-  destruct op; destruct eq_operation; intros; simpl in *; try congruence.
+  destruct op; destruct eq_operation; intros; cbn in *; try congruence.
   all: try (destruct vl as [ | vh1 vl1]; try discriminate).
   all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
@@ -1101,7 +1101,7 @@ Lemma eval_negate_condition:
   forall cond vl m,
   eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m).
 Proof.
-  intros. destruct cond; simpl.
+  intros. destruct cond; cbn.
   repeat (destruct vl; auto). apply Val.negate_cmp_bool.
   repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
   repeat (destruct vl; auto). apply Val.negate_cmp_bool.
@@ -1147,7 +1147,7 @@ Lemma eval_shift_stack_addressing:
   eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
   eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl.
 Proof.
-  intros. destruct addr; simpl; auto. destruct vl; auto.
+  intros. destruct addr; cbn; auto. destruct vl; auto.
   rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
 Qed.
 
@@ -1156,7 +1156,7 @@ Lemma eval_shift_stack_operation:
   eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m =
   eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m.
 Proof.
-  intros. destruct op; simpl; auto. destruct vl; auto.
+  intros. destruct op; cbn; auto. destruct vl; auto.
   rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
 Qed.
 
@@ -1183,12 +1183,12 @@ Proof.
   assert (A: forall x n,
              Val.offset_ptr x (Ptrofs.add n (Ptrofs.repr delta)) =
              Val.add (Val.offset_ptr x n) (Vint (Int.repr delta))).
-  { intros; destruct x; simpl; auto. rewrite H1. 
+  { intros; destruct x; cbn; auto. rewrite H1. 
     rewrite Ptrofs.add_assoc. f_equal; f_equal; f_equal. symmetry; auto with ptrofs. }
-  destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
+  destruct addr; cbn in H; inv H; cbn in *; FuncInv; subst.
 - rewrite A; auto.
 - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. 
-  simpl. rewrite H1. f_equal; f_equal; f_equal. symmetry; auto with ptrofs.
+  cbn. rewrite H1. f_equal; f_equal; f_equal. symmetry; auto with ptrofs.
 - rewrite A; auto.
 Qed.
 
@@ -1223,17 +1223,17 @@ Lemma op_depends_on_memory_correct:
   op_depends_on_memory op = false ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros until m2. destruct op; simpl; try congruence.
-  - destruct cond; simpl; try congruence;
+  intros until m2. destruct op; cbn; try congruence.
+  - destruct cond; cbn; try congruence;
     intros SF; auto; rewrite ? negb_false_iff in SF;
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
-  - destruct c0; simpl; try congruence;
+  - destruct c0; cbn; try congruence;
     intros SF; auto; rewrite ? negb_false_iff in SF;
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
-  - destruct c0; simpl; try congruence;
+  - destruct c0; cbn; try congruence;
     intros SF; auto; rewrite ? negb_false_iff in SF;
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
-  - destruct c0; simpl; try congruence;
+  - destruct c0; cbn; try congruence;
     intros SF; auto; rewrite ? negb_false_iff in SF;
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
@@ -1348,19 +1348,19 @@ Lemma eval_condition_inj:
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
-  intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
+  intros. destruct cond; cbn in H0; FuncInv; InvInject; cbn; auto.
+- inv H3; inv H2; cbn in H0; inv H0; auto.
 - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
-- inv H3; simpl in H0; inv H0; auto.
+- inv H3; cbn in H0; inv H0; auto.
 - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; inv H2; cbn in H0; inv H0; auto.
 - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
-- inv H3; simpl in H0; inv H0; auto.
+- inv H3; cbn in H0; inv H0; auto.
 - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
-- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; inv H2; cbn in H0; inv H0; auto.
+- inv H3; inv H2; cbn in H0; inv H0; auto.
+- inv H3; inv H2; cbn in H0; inv H0; auto.
+- inv H3; inv H2; cbn in H0; inv H0; auto.
 Qed.
 
 Lemma eval_condition0_inj:
@@ -1369,10 +1369,10 @@ Lemma eval_condition0_inj:
   eval_condition0 cond v1 m1 = Some b ->
   eval_condition0 cond v2 m2 = Some b.
 Proof.
-  intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
-  - inv H; simpl in *; congruence.
+  intros. destruct cond; cbn in H0; FuncInv; InvInject; cbn; auto.
+  - inv H; cbn in *; congruence.
   - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
-  - inv H; simpl in *; congruence.
+  - inv H; cbn in *; congruence.
   - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
 Qed.
 
@@ -1393,248 +1393,244 @@ Lemma eval_operation_inj:
   eval_operation ge1 sp1 op vl1 m1 = Some v1 ->
   exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
-  intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
+  intros until v1; intros GL; intros. destruct op; cbn in H1; cbn; FuncInv; InvInject; TrivialExists.
   (* addrsymbol *)
-  - apply GL; simpl; auto.
+  - apply GL; cbn; auto.
   (* addrstack *)
   - apply Val.offset_ptr_inject; auto. 
   (* castsigned *)
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* add, addimm *)
   - apply Val.add_inject; auto.
   - apply Val.add_inject; auto.
   (* addx, addximm *)
   - apply Val.add_inject; trivial.
-    inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto.
-  - inv H4; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
+    inv H4; inv H2; cbn; try destruct (Int.ltu _ _); cbn; auto.
+  - inv H4; cbn; trivial.
+    destruct (Int.ltu _ _); cbn; trivial.
   (* neg, sub *)
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
   - apply Val.sub_inject; auto.
   (* revsubimm, revsubx, revsubximm *)
-  - inv H4; simpl; trivial.
+  - inv H4; cbn; trivial.
   - apply Val.sub_inject; trivial.
-    inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto.
-  - inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto.
+    inv H4; inv H2; cbn; try destruct (Int.ltu _ _); cbn; auto.
+  - inv H4; cbn; try destruct (Int.ltu _ _); cbn; auto.
   (* mul, mulimm, mulhs, mulhu *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
   (* div, divu *)
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int.eq i0 Int.zero
-              || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2.
+  - inv H4; inv H3; cbn in H1; inv H1. cbn.
+    destruct (_ || _); inv H2.
     TrivialExists.
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
+  - inv H4; inv H3; cbn in H1; inv H1. cbn.
     destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
   (* mod, modu *)
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int.eq i0 Int.zero
-                     || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2.
+  - inv H4; inv H3; cbn in H1; inv H1. cbn.
+    destruct (_ || _); inv H2.
     TrivialExists.
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
+  - inv H4; inv H3; cbn in H1; inv H1. cbn.
     destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
   (* and, andimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* nand, nandimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* or, orimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* nor, norimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* xor, xorimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* nxor, nxorimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* not *)
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
   (* andn, andnimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* orn, ornimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* shl, shlimm *)
-  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
-  - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
+  - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
+  - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto.
   (* shr, shrimm *)
-  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
-  - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
+  - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
+  - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto.
   (* shru, shruimm *)
-  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
-  - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
+  - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
+  - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto.
   (* shrx *)
-  - inv H4; simpl; auto.
-    destruct (Int.ltu n (Int.repr 31)); inv H; simpl; auto.
+  - inv H4; cbn; auto.
+    destruct (Int.ltu n (Int.repr 31)); inv H; cbn; auto.
   (* rorimm *)
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
   (* madd, maddim *)
-  - inv H2; inv H3; inv H4; simpl; auto.
-  - inv H2; inv H4; simpl; auto.
+  - inv H2; inv H3; inv H4; cbn; auto.
+  - inv H2; inv H4; cbn; auto.
   (* msub *)
   - apply Val.sub_inject; auto.
-    inv H3; inv H2; simpl; auto.
+    inv H3; inv H2; cbn; auto.
   (* makelong, highlong, lowlong *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* cast32 *)
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* addl, addlimm *)
   - apply Val.addl_inject; auto.
   - apply Val.addl_inject; auto.
   (* addxl, addxlimm *)
   - apply Val.addl_inject; auto.
-    inv H4; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
-  - inv H4; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
+    inv H4; cbn; trivial.
+    destruct (Int.ltu _ _); cbn; trivial.
+  - inv H4; cbn; trivial.
+    destruct (Int.ltu _ _); cbn; trivial.
   (* negl, subl *)
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
   - apply Val.subl_inject; auto.
-    inv H4; inv H2; simpl; trivial;
-    destruct (Int.ltu _ _); simpl; trivial.
-  - inv H4; simpl; trivial;
-      destruct (Int.ltu _ _); simpl; trivial.
-  - inv H4; simpl; auto.
+    inv H4; inv H2; cbn; trivial;
+    destruct (Int.ltu _ _); cbn; trivial.
+  - inv H4; cbn; trivial;
+      destruct (Int.ltu _ _); cbn; trivial.
+  - inv H4; cbn; auto.
   - apply Val.subl_inject; auto.
   (* mull, mullhs, mullhu *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
   (* divl, divlu *)
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int64.eq i0 Int64.zero
-              || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2.
+  - inv H4; inv H3; cbn in H1; inv H1. cbn.
+    destruct (_ || _); inv H2.
     TrivialExists.
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
+  - inv H4; inv H3; cbn in H1; inv H1. cbn.
     destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists.
   (* modl, modlu *)
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int64.eq i0 Int64.zero
-                     || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2.
+  - inv H4; inv H3; cbn in H1; inv H1. cbn.
+    destruct (_ || _); inv H2.
     TrivialExists.
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
+  - inv H4; inv H3; cbn in H1; inv H1. cbn.
     destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists.
   (* andl, andlimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* nandl, nandlimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* orl, orlimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* norl, norlimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* xorl, xorlimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* nxorl, nxorlimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* notl *)
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
   (* andnl, andnlimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* ornl, ornlimm *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; cbn; auto.
   (* shll, shllimm *)
-  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
-  - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
+  - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
   (* shr, shrimm *)
-  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
-  - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
+  - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
   (* shru, shruimm *)
-  - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
-  - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
+  - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
   (* shrx *)
-  - inv H4; simpl; auto.
-    destruct (Int.ltu n (Int.repr 63)); simpl; auto.
+  - inv H4; cbn; auto.
+    destruct (Int.ltu n (Int.repr 63)); cbn; auto.
 
   (* maddl, maddlimm *)
   - apply Val.addl_inject; auto.
-    inv H2; inv H3; inv H4; simpl; auto.
+    inv H2; inv H3; inv H4; cbn; auto.
   - apply Val.addl_inject; auto.
-    inv H4; inv H2; simpl; auto.
+    inv H4; inv H2; cbn; auto.
   (* msubl, msublimm *)
   - apply Val.subl_inject; auto.
-    inv H2; inv H3; inv H4; simpl; auto.
+    inv H2; inv H3; inv H4; cbn; auto.
     
   (* negf, absf *)
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* addf, subf *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
   (* mulf, divf *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
   (* minf, maxf *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
   (* fmaddf, fmsubf *)
-  - inv H4; inv H3; inv H2; simpl; auto.
-  - inv H4; inv H3; inv H2; simpl; auto.
+  - inv H4; inv H3; inv H2; cbn; auto.
+  - inv H4; inv H3; inv H2; cbn; auto.
   (* negfs, absfs *)
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* addfs, subfs *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
   (* mulfs, divfs *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
   (* minfs, maxfs *)
-  - inv H4; inv H2; simpl; auto.
-  - inv H4; inv H2; simpl; auto.
+  - inv H4; inv H2; cbn; auto.
+  - inv H4; inv H2; cbn; auto.
   (* invfs *)
-  - inv H4; simpl; auto.    
+  - inv H4; cbn; auto.    
   (* fmaddfs, fmsubfs *)
-  - inv H4; inv H3; inv H2; simpl; auto.
-  - inv H4; inv H3; inv H2; simpl; auto.
+  - inv H4; inv H3; inv H2; cbn; auto.
+  - inv H4; inv H3; inv H2; cbn; auto.
   (* singleoffloat, floatofsingle *)
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* intoffloat, intuoffloat *)
-  - inv H4; simpl; auto. destruct (Float.to_int f0); simpl; auto.
-  - inv H4; simpl; auto. destruct (Float.to_intu f0); simpl; auto.
+  - inv H4; cbn; auto. destruct (Float.to_int f0); cbn; auto.
+  - inv H4; cbn; auto. destruct (Float.to_intu f0); cbn; auto.
   (* intofsingle, intuofsingle *)
-  - inv H4; simpl; auto. destruct (Float32.to_int f0); simpl; auto.
-  - inv H4; simpl; auto. destruct (Float32.to_intu f0); simpl; auto.
+  - inv H4; cbn; auto. destruct (Float32.to_int f0); cbn; auto.
+  - inv H4; cbn; auto. destruct (Float32.to_intu f0); cbn; auto.
   (* singleofint, singleofintu *)
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* longoffloat, longuoffloat *)
-  - inv H4; simpl; auto. destruct (Float.to_long f0); simpl; auto.
-  - inv H4; simpl; auto. destruct (Float.to_longu f0); simpl; auto.
+  - inv H4; cbn; auto. destruct (Float.to_long f0); cbn; auto.
+  - inv H4; cbn; auto. destruct (Float.to_longu f0); cbn; auto.
   (* floatoflong, floatoflongu *)
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* longofsingle, longuofsingle *)
-  - inv H4; simpl; auto. destruct (Float32.to_long f0); simpl; auto.
-  - inv H4; simpl; auto. destruct (Float32.to_longu f0); simpl; auto.
+  - inv H4; cbn; auto. destruct (Float32.to_long f0); cbn; auto.
+  - inv H4; cbn; auto. destruct (Float32.to_longu f0); cbn; auto.
   (* singleoflong, singleoflongu *)
-  - inv H4; simpl; auto.
-  - inv H4; simpl; auto.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* cmp *)
   - subst v1. destruct (eval_condition cond vl1 m1) eqn:?.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
-    destruct b; simpl; constructor.
-    simpl; constructor.
+    destruct b; cbn; constructor.
+    cbn; constructor.
 
  (* extfz *)
   - unfold extfz.
@@ -1664,16 +1660,16 @@ Proof.
   - unfold insf.
     destruct (is_bitfield _ _).
     + inv H4; inv H2; trivial.
-      simpl. destruct (Int.ltu _ _); trivial.
-      simpl. trivial.
+      cbn. destruct (Int.ltu _ _); trivial.
+      cbn. trivial.
     + trivial.
 
  (* insfl *)
   - unfold insfl.
     destruct (is_bitfieldl _ _).
     + inv H4; inv H2; trivial.
-      simpl. destruct (Int.ltu _ _); trivial.
-      simpl. trivial.
+      cbn. destruct (Int.ltu _ _); trivial.
+      cbn. trivial.
     + trivial.
 
  (* Osel *)
@@ -1711,13 +1707,13 @@ Lemma eval_addressing_inj:
   eval_addressing ge1 sp1 addr vl1 = Some v1 ->
   exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
-  intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
+  intros. destruct addr; cbn in H2; cbn; FuncInv; InvInject; TrivialExists.
   - apply Val.addl_inject; trivial.
-    destruct v0; destruct v'0; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial; inv H3.
+    destruct v0; destruct v'0; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial; inv H3.
     apply Val.inject_long.
   - apply Val.addl_inject; auto.
   - apply Val.offset_ptr_inject; auto.
-  - apply H; simpl; auto.
+  - apply H; cbn; auto.
   - apply Val.offset_ptr_inject; auto. 
 Qed.
 
@@ -1732,7 +1728,7 @@ Lemma eval_addressing_inj_none:
   eval_addressing ge2 sp2 addr vl2 = None.
 Proof.
   intros until vl2. intros Hglobal Hinjsp Hinjvl.
-  destruct addr; simpl in *.
+  destruct addr; cbn in *.
   1,2: inv Hinjvl; trivial;
        inv H0; trivial;
        inv H2; trivial;
@@ -1856,7 +1852,7 @@ Lemma eval_addressing_lessdef_none:
   eval_addressing genv sp addr vl2 = None.
 Proof.
   intros until vl2. intros Hlessdef Heval1.
-  destruct addr; simpl in *.
+  destruct addr; cbn in *.
   1, 2, 4, 5: inv Hlessdef; trivial;
   inv H0; trivial;
   inv H2; trivial;
@@ -1941,7 +1937,7 @@ Lemma eval_operation_inject:
   /\ Val.inject f v1 v2.
 Proof.
   intros.
-  rewrite eval_shift_stack_operation. simpl.
+  rewrite eval_shift_stack_operation. cbn.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.