From 183112fc6a5fbb7d1c6d60b9717cdb8aceda78ca Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Mon, 8 Sep 2014 16:19:39 +0200 Subject: Simpl less (so that cbn will not simpl too much) --- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 27 ++++++++------- theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 3 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 1 + theories/Numbers/Cyclic/Int31/Cyclic31.v | 41 +++++++++++------------ theories/Numbers/Natural/BigN/NMake.v | 2 +- 7 files changed, 38 insertions(+), 40 deletions(-) (limited to 'theories/Numbers') 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. -- cgit v1.2.3