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) --- plugins/btauto/Reflect.v | 6 ++-- plugins/micromega/RMicromega.v | 5 ++- theories/Arith/Div2.v | 2 +- theories/FSets/FMapAVL.v | 10 +++--- theories/MSets/MSetGenTree.v | 4 +-- theories/MSets/MSetRBT.v | 6 ++-- theories/NArith/Nnat.v | 4 +-- 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 +- theories/PArith/BinPos.v | 2 +- theories/PArith/BinPosDef.v | 2 +- theories/PArith/Pnat.v | 5 +-- theories/ZArith/Zlogarithm.v | 2 +- theories/ZArith/Zpow_facts.v | 4 +-- 19 files changed, 63 insertions(+), 67 deletions(-) diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 8a95d5b4b..3bd7cd622 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -196,9 +196,9 @@ Qed. Lemma make_last_nth_1 : forall A n i x def, i <> n -> list_nth i (@make_last A n x def) def = def. Proof. -intros A n; induction n using Pos.peano_rect; intros i x def Hd; simpl. -+ unfold make_last; rewrite Pos.peano_rect_base. - induction i using Pos.peano_case; [elim Hd; reflexivity|]. +intros A n; induction n using Pos.peano_rect; intros i x def Hd; + unfold make_last; simpl. ++ induction i using Pos.peano_case; [elim Hd; reflexivity|]. rewrite list_nth_succ, list_nth_nil; reflexivity. + unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def). induction i using Pos.peano_case. diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index d6f674858..f4b4dd661 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -243,7 +243,6 @@ Proof. unfold IQR ; intros. simpl. repeat rewrite mult_IZR. - simpl. rewrite Pos2Nat.inj_mul. rewrite mult_INR. repeat INR_nat_of_P. @@ -260,8 +259,8 @@ Proof. simpl. intros. unfold Qinv. - destruct x ; simpl in *. - destruct Qnum ; simpl. + destruct x. + destruct Qnum ; simpl in *. exfalso. auto with zarith. clear H. repeat INR_nat_of_P. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 8cef48b69..a9d77c90d 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -110,7 +110,7 @@ Proof. split; split; auto with arith. inversion_clear 1. inversion H0. - (* n = (S (S n')) *) destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')). - split; split; simpl; rewrite ?double_S. + split; split; simpl div2; rewrite ?double_S. + inversion_clear 1. inversion_clear H0. auto. + injection 1. auto with arith. + inversion_clear 1. inversion_clear H0. auto. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index fe08960ad..c9e5b8dd2 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1433,14 +1433,14 @@ Lemma flatten_e_elements : elements l ++ flatten_e (More x d r e) = elements (Node l x d r z) ++ flatten_e e. Proof. - intros; simpl; apply elements_node. + intros; apply elements_node. Qed. Lemma cons_1 : forall (s:t elt) e, flatten_e (cons s e) = elements s ++ flatten_e e. Proof. - induction s; simpl; auto; intros. - rewrite IHs1; apply flatten_e_elements; auto. + induction s; auto; intros. + simpl flatten_e; rewrite IHs1; apply flatten_e_elements; auto. Qed. (** Proof of correction for the comparison *) @@ -1478,7 +1478,7 @@ Lemma equal_cont_IfEq : forall m1 cont e2 l, (forall e, IfEq (cont e) l (flatten_e e)) -> IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2). Proof. - induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto. + induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto. rewrite <- elements_node; simpl. apply Hl1; auto. clear e2; intros [|x2 d2 r2 e2]. @@ -2084,7 +2084,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: (forall e, Cmp (cont e) l (P.flatten_e e)) -> Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2). Proof. - induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto. + induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto. rewrite <- P.elements_node; simpl. apply Hl1; auto. clear e2. intros [|x2 d2 r2 e2]. simpl; auto. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index d1d9897fb..154c2384c 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -1019,7 +1019,7 @@ Lemma flatten_e_elements : forall l x r c e, elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e. Proof. - intros; simpl. now rewrite elements_node, app_ass. + intros. now rewrite elements_node, app_ass. Qed. Lemma cons_1 : forall s e, @@ -1053,7 +1053,7 @@ Lemma compare_cont_Cmp : forall s1 cont e2 l, (forall e, Cmp (cont e) l (flatten_e e)) -> Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2). Proof. - induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; simpl; intros; auto. + induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; intros; auto. rewrite elements_node, app_ass; simpl. apply Hl1; auto. clear e2. intros [|x2 r2 e2]. simpl; auto. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index d7e56cdef..751d4f35c 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -987,7 +987,7 @@ Proof. rewrite app_length, <- elements_cardinal. simpl. rewrite Nat.add_succ_r, <- Nat.succ_le_mono. apply Nat.add_le_mono_l. } - simpl. rewrite elements_node, app_ass. now subst. + rewrite elements_node, app_ass. now subst. Qed. Lemma treeify_aux_spec n (p:bool) : @@ -1012,7 +1012,7 @@ Qed. Lemma plength_aux_spec l p : Pos.to_nat (plength_aux l p) = length l + Pos.to_nat p. Proof. - revert p. induction l; simpl; trivial. + revert p. induction l; trivial. simpl plength_aux. intros. now rewrite IHl, Pos2Nat.inj_succ, Nat.add_succ_r. Qed. @@ -1058,7 +1058,7 @@ Lemma filter_aux_elements s f acc : filter_aux f s acc = List.filter f (elements s) ++ acc. Proof. revert acc. - induction s as [|c l IHl x r IHr]; simpl; trivial. + induction s as [|c l IHl x r IHr]; trivial. intros acc. rewrite elements_node, filter_app. simpl. destruct (f x); now rewrite IHl, IHr, app_ass. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 94242394b..6551f6c10 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -84,8 +84,8 @@ Qed. Lemma inj_div2 a : N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a). Proof. destruct a as [|[p|p| ]]; trivial. - - simpl N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double. - - simpl N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double. + - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double. + - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double. Qed. Lemma inj_compare a a' : 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. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index a30c555c1..0f794c513 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -649,7 +649,7 @@ Theorem sub_mask_carry_spec p q : sub_mask_carry p q = pred_mask (sub_mask p q). Proof. revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl; - try reflexivity; try rewrite IHp; + try reflexivity; rewrite ?IHp; destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto. Qed. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index fcc12ab45..44b9e7d03 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -537,7 +537,7 @@ Definition iter_op {A}(op:A->A->A) := end. Definition to_nat (x:positive) : nat := iter_op plus x (S O). - +Arguments to_nat x: simpl never. (** ** From Peano natural numbers to binary positive numbers *) (** A version preserving positive numbers, and sending 0 to 1. *) diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index 4336d47af..0f2ecf55a 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -196,7 +196,8 @@ Theorem inj_iter : Proof. induction p using peano_ind. - trivial. - - intros. rewrite inj_succ, iter_succ. simpl. now f_equal. + - intros. rewrite inj_succ, iter_succ. + simpl. f_equal. apply IHp. Qed. End Pos2Nat. @@ -210,7 +211,7 @@ Module Nat2Pos. Theorem id (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n. Proof. induction n as [|n H]; trivial. now destruct 1. - intros _. simpl. destruct n. trivial. + intros _. simpl Pos.of_nat. destruct n. trivial. rewrite Pos2Nat.inj_succ. f_equal. now apply H. Qed. diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 319e2c269..23b692022 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -59,7 +59,7 @@ Section Log_pos. (* Log of positive integers *) Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p. Proof. - induction p; simpl. + induction p; simpl log_sup. - change (Zpos p~1) with (2*(Zpos p)+1). rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy. unfold Z.succ. now rewrite !(Z.add_comm _ 1), Z.add_assoc. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 8ff641a33..5b0e3ef5e 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -152,10 +152,8 @@ Qed. Theorem Zpow_mod_correct a m n : n <> 0 -> Zpow_mod a m n = (a ^ m) mod n. Proof. - intros Hn. destruct m; simpl. - - trivial. + intros Hn. destruct m; simpl; trivial. - apply Zpow_mod_pos_correct; auto with zarith. - - rewrite Z.mod_0_l; auto with zarith. Qed. (* Complements about power and number theory. *) -- cgit v1.2.3