Simpl less (so that cbn will not simpl too much)

7 files changed, 38 insertions, 40 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index c9f3a774d..7594b0478 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -106,7 +106,7 @@ Qed.
 
 Theorem one_succ : one == succ zero.
 Proof.
-zify; simpl. now rewrite one_mod_wB.
+zify; simpl Z.add. now rewrite one_mod_wB.
 Qed.
 
 Theorem two_succ : two == succ one.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index 35d8b595c..e14c3b829 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
@@ -194,9 +194,9 @@ Section DoubleAdd.
 
   Lemma spec_ww_add_c  : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]].
   Proof.
-   destruct x as [ |xh xl];simpl;trivial.
-   destruct y as [ |yh yl];simpl. rewrite Z.add_0_r;trivial.
-   replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]))
+   destruct x as [ |xh xl];trivial.
+   destruct y as [ |yh yl]. rewrite Z.add_0_r;trivial.
+   simpl. replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]))
    with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|])). 2:ring.
    generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l];
     intros H;unfold interp_carry in H;rewrite <- H.
@@ -218,10 +218,11 @@ Section DoubleAdd.
 
    Lemma spec_ww_add_c_cont  : P x y (ww_add_c_cont x y).
    Proof.
-    destruct x as [ |xh xl];simpl;trivial.
+    destruct x as [ |xh xl];trivial.
     apply spec_f0;trivial.
-    destruct y as [ |yh yl];simpl.
-    apply spec_f0;simpl;rewrite Z.add_0_r;trivial.
+    destruct y as [ |yh yl].
+    apply spec_f0;rewrite Z.add_0_r;trivial.
+    simpl.
     generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l];
      intros H;unfold interp_carry in H.
     generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h];
@@ -234,10 +235,10 @@ Section DoubleAdd.
      as [h|h]; intros H1;unfold interp_carry in *.
     apply spec_f0;simpl;rewrite H1. rewrite Z.mul_add_distr_r.
     rewrite <- Z.add_assoc;rewrite H;ring.
-    apply spec_f1.  simpl;rewrite spec_w_WW;rewrite wwB_wBwB.
+    apply spec_f1. rewrite spec_w_WW;rewrite wwB_wBwB.
     rewrite Z.add_assoc; rewrite Z.pow_2_r; rewrite <- Z.mul_add_distr_r.
     rewrite Z.mul_1_l in H1;rewrite H1. rewrite Z.mul_add_distr_r.
-    rewrite <- Z.add_assoc;rewrite H;ring.
+    rewrite <- Z.add_assoc;rewrite H; simpl; ring.
    Qed.
 
   End Cont.
@@ -245,11 +246,11 @@ Section DoubleAdd.
   Lemma spec_ww_add_carry_c :
          forall x y, [+[ww_add_carry_c x y]] = [[x]] + [[y]] + 1.
   Proof.
-   destruct x as [ |xh xl];intro y;simpl.
+   destruct x as [ |xh xl];intro y.
    exact (spec_ww_succ_c y).
-   destruct y as [ |yh yl];simpl.
+   destruct y as [ |yh yl].
    rewrite Z.add_0_r;exact (spec_ww_succ_c (WW xh xl)).
-   replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1)
+   simpl; replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1)
    with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|]+1)). 2:ring.
    generalize (spec_w_add_carry_c xl yl);destruct (w_add_carry_c xl yl)
     as [l|l];intros H;unfold interp_carry in H;rewrite <- H.
@@ -281,7 +282,7 @@ Section DoubleAdd.
 
   Lemma spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB.
   Proof.
-   destruct x as [ |xh xl];intros y;simpl.
+   destruct x as [ |xh xl];intros y.
    rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial.
    destruct y as [ |yh yl].
    change [[W0]] with 0;rewrite Z.add_0_r.
@@ -299,7 +300,7 @@ Section DoubleAdd.
   Lemma spec_ww_add_carry :
 	 forall x y, [[ww_add_carry x y]] = ([[x]] + [[y]] + 1) mod wwB.
   Proof.
-   destruct x as [ |xh xl];intros y;simpl.
+   destruct x as [ |xh xl];intros y.
    exact (spec_ww_succ y).
    destruct y as [ |yh yl].
    change [[W0]] with 0;rewrite Z.add_0_r. exact (spec_ww_succ (WW xh xl)).
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index dddae7db5..20b55a4c6 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -97,8 +97,7 @@ Section POS_MOD.
  assert (HHHHH:= lt_0_wB w_digits).
  assert (F0: forall x y, x - y + y = x); auto with zarith.
  intros w1 p; case (spec_to_w_Z p); intros HH1 HH2.
- unfold ww_pos_mod; case w1.
- simpl; rewrite Zmod_small; split; auto with zarith.
+ unfold ww_pos_mod; case w1. reflexivity.
  intros xh xl; rewrite spec_ww_compare.
     case Z.compare_spec;
     rewrite spec_w_0W; rewrite spec_zdigits; fold wB;
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 789436334..5ca332551 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -266,8 +266,8 @@ Section DoubleSqrt.
       if ww_is_even x then [[x]] mod 2 = 0 else [[x]] mod 2 = 1.
 clear spec_more_than_1_digit.
 intros x; case x; simpl ww_is_even.
+ reflexivity.
  simpl.
- rewrite Zmod_small; auto with zarith.
  intros w1 w2; simpl.
  unfold base.
  rewrite Zplus_mod; auto with zarith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 900cb1db5..fad488beb 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -14,6 +14,7 @@ Require Import ZArith.
 Local Open Scope Z_scope.
 
 Definition base digits := Z.pow 2 (Zpos digits).
+Arguments base digits: simpl never.
 
 Section Carry.
 
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 98f84a60c..f6669d284 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1414,7 +1414,7 @@ Section Int31_Specs.
  generalize (phi_bounded a1)(phi_bounded a2)(phi_bounded b); intros.
  assert ([|b|]>0) by (auto with zarith).
  generalize (Z_div_mod (phi2 a1 a2) [|b|] H4) (Z_div_pos (phi2 a1 a2) [|b|] H4).
- unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]); simpl.
+ unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]).
  rewrite ?phi_phi_inv.
  destruct 1; intros.
  unfold phi2 in *.
@@ -1444,7 +1444,7 @@ Section Int31_Specs.
  unfold div31; intros.
  assert ([|b|]>0) by (auto with zarith).
  generalize (Z_div_mod [|a|] [|b|] H0) (Z_div_pos [|a|] [|b|] H0).
- unfold Z.div; destruct (Z.div_eucl [|a|] [|b|]); simpl.
+ unfold Z.div; destruct (Z.div_eucl [|a|] [|b|]).
  rewrite ?phi_phi_inv.
  destruct 1; intros.
  rewrite H1, Z.mul_comm.
@@ -1467,7 +1467,7 @@ Section Int31_Specs.
  assert ([|b|]>0) by (auto with zarith).
  unfold Z.modulo.
  generalize (Z_div_mod [|a|] [|b|] H0).
- destruct (Z.div_eucl [|a|] [|b|]); simpl.
+ destruct (Z.div_eucl [|a|] [|b|]).
  rewrite ?phi_phi_inv.
  destruct 1; intros.
  generalize (phi_bounded b); intros.
@@ -1480,15 +1480,14 @@ Section Int31_Specs.
   unfold gcd31.
   induction (2*size)%nat; intros.
   reflexivity.
-  simpl.
+  simpl euler.
   unfold compare31.
   change [|On|] with 0.
   generalize (phi_bounded j)(phi_bounded i); intros.
   case_eq [|j|]; intros.
   simpl; intros.
   generalize (Zabs_spec [|i|]); omega.
-  simpl.
-  rewrite IHn, H1; f_equal.
+  simpl. rewrite IHn, H1; f_equal.
   rewrite spec_mod, H1; auto.
   rewrite H1; compute; auto.
   rewrite H1 in H; destruct H as [H _]; compute in H; elim H; auto.
@@ -1521,7 +1520,7 @@ Section Int31_Specs.
  simpl; auto.
  simpl; intros.
  case_eq (firstr i); intros H; rewrite 2 IHn;
-  unfold phibis_aux; simpl; rewrite H; fold (phibis_aux n (shiftr i));
+  unfold phibis_aux; simpl; rewrite ?H; fold (phibis_aux n (shiftr i));
   generalize (phibis_aux_pos n (shiftr i)); intros;
   set (z := phibis_aux n (shiftr i)) in *; clearbody z;
   rewrite <- nat_rect_plus.
@@ -1575,10 +1574,9 @@ Section Int31_Specs.
  clear p H; revert x y.
 
  induction n.
- simpl; intros.
- change (Z.pow_pos 2 31) with (2^31).
+ simpl Z.of_nat; intros.
  rewrite Z.mul_1_r.
- replace ([|y|] / 2^31) with 0.
+ replace ([|y|] / 2^(31-0)) with 0.
  rewrite Z.add_0_r.
  symmetry; apply Zmod_small; apply phi_bounded.
  symmetry; apply Zdiv_small; apply phi_bounded.
@@ -1666,7 +1664,7 @@ Section Int31_Specs.
  Proof.
   intros.
   generalize (phi_inv_phi x).
-  rewrite H; simpl.
+  rewrite H; simpl phi_inv.
   intros H'; rewrite <- H'.
   simpl; auto.
  Qed.
@@ -1774,7 +1772,7 @@ Section Int31_Specs.
  Proof.
   intros.
   generalize (phi_inv_phi x).
-  rewrite H; simpl.
+  rewrite H; simpl phi_inv.
   intros H'; rewrite <- H'.
   simpl; auto.
  Qed.
@@ -2121,7 +2119,7 @@ Section Int31_Specs.
  unfold phi2; rewrite Hc1.
  assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith).
  rewrite Z.mul_comm, Z_div_plus_full_l; unfold base; auto with zarith.
- unfold Z.pow, Z.pow_pos in Hj1; simpl in Hj1; auto with zarith.
+ simpl wB in Hj1. unfold Z.pow_pos in Hj1. simpl in Hj1. auto with zarith.
  case (Z.le_gt_cases (2 ^ 30) [|j|]); intros Hjj.
  rewrite spec_compare; case Z.compare_spec;
   rewrite div312_phi; auto; intros Hc;
@@ -2260,9 +2258,8 @@ Section Int31_Specs.
  intros Hihl1.
  generalize (spec_sub_c il il1).
  case sub31c; intros il2 Hil2.
- simpl interp_carry in Hil2.
  rewrite spec_compare; case Z.compare_spec.
- unfold interp_carry.
+ unfold interp_carry in *.
  intros H1; split.
  rewrite Z.pow_2_r, <- Hihl1.
  unfold phi2; ring[Hil2 H1].
@@ -2279,7 +2276,7 @@ Section Int31_Specs.
  rewrite Z.mul_add_distr_r, Z.add_0_r; auto with zarith.
  case (phi_bounded il1); intros H3 _.
  apply Z.add_le_mono; auto with zarith.
- unfold interp_carry; change (1 * 2 ^ Z.of_nat size) with base.
+ unfold interp_carry in *; change (1 * 2 ^ Z.of_nat size) with base.
  rewrite Z.pow_2_r, <- Hihl1, Hil2.
  intros H1.
  rewrite <- Z.le_succ_l, <- Z.add_1_r in H1.
@@ -2383,8 +2380,8 @@ Qed.
 
  Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [|x|] = 0.
  Proof.
- clear; unfold ZnZ.eq0; simpl.
- unfold compare31; simpl; intros.
+ clear; unfold ZnZ.eq0, int31_ops.
+ unfold compare31; intros.
  change [|0|] with 0 in H.
  apply Z.compare_eq.
  now destruct ([|x|] ?= 0).
@@ -2395,7 +2392,7 @@ Qed.
  Lemma spec_is_even : forall x,
       if ZnZ.is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
  Proof.
- unfold ZnZ.is_even; simpl; intros.
+ unfold ZnZ.is_even, int31_ops; intros.
  generalize (spec_div x 2).
  destruct (x/2)%int31 as (q,r); intros.
  unfold compare31.
@@ -2420,7 +2417,7 @@ Qed.
 
  Lemma spec_lor x y : [| ZnZ.lor x y |] = Z.lor [|x|] [|y|].
  Proof.
- unfold ZnZ.lor; simpl. unfold lor31.
+ unfold ZnZ.lor,int31_ops. unfold lor31.
  rewrite phi_phi_inv.
  apply Z.mod_small; split; trivial.
  - apply Z.lor_nonneg; split; apply phi_bounded.
@@ -2431,7 +2428,7 @@ Qed.
 
  Lemma spec_land x y : [| ZnZ.land x y |] = Z.land [|x|] [|y|].
  Proof.
- unfold ZnZ.land; simpl. unfold land31.
+ unfold ZnZ.land, int31_ops. unfold land31.
  rewrite phi_phi_inv.
  apply Z.mod_small; split; trivial.
  - apply Z.land_nonneg; left; apply phi_bounded.
@@ -2443,7 +2440,7 @@ Qed.
 
  Lemma spec_lxor x y : [| ZnZ.lxor x y |] = Z.lxor [|x|] [|y|].
  Proof.
- unfold ZnZ.lxor; simpl. unfold lxor31.
+ unfold ZnZ.lxor, int31_ops. unfold lxor31.
  rewrite phi_phi_inv.
  apply Z.mod_small; split; trivial.
  - apply Z.lxor_nonneg; split; intros; apply phi_bounded.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index bfbcb9465..dab2399c9 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -146,7 +146,7 @@ Module Make (W0:CyclicType) <: NType.
  Theorem spec_add: forall x y, [add x y] = [x] + [y].
  Proof.
   intros x y. rewrite add_fold. apply spec_same_level; clear x y.
-  intros n x y. simpl.
+  intros n x y. cbv beta iota zeta.
   generalize (ZnZ.spec_add_c x y); case ZnZ.add_c; intros z H.
   rewrite spec_mk_t. assumption.
   rewrite spec_mk_t_S. unfold interp_carry in H.