diff options
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPow.v | 49 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 |
4 files changed, 9 insertions, 62 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 4f88008be4..6e6cd7f0fc 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -70,26 +70,16 @@ Module Type Parity (Import Z : ZAxiomsMiniSig'). Axiom odd_spec : forall n, odd n = true <-> Odd n. End Parity. -(** For the power function, we just add to NZPow an addition spec *) - -Module Type ZPowSpecNeg (Import Z : ZAxiomsMiniSig')(Import P : Pow' Z). - Axiom pow_neg : forall a b, b<0 -> a^b == 0. -End ZPowSpecNeg. - -(** Same for the sqrt function. *) - -Module Type ZSqrtSpecNeg (Import Z : ZAxiomsMiniSig')(Import P : Sqrt' Z). - Axiom sqrt_neg : forall a, a<0 -> √a == 0. -End ZSqrtSpecNeg. +(** For the power and sqrt functions, the NZ axiomatizations are enough. *) (** Let's group everything *) Module Type ZAxiomsSig := ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow <+ ZPowSpecNeg <+ NZSqrt.NZSqrt <+ ZSqrtSpecNeg. + <+ NZPow.NZPow <+ NZSqrt.NZSqrt. Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow' <+ ZPowSpecNeg <+ NZSqrt.NZSqrt' <+ ZSqrtSpecNeg. + <+ NZPow.NZPow' <+ NZSqrt.NZSqrt'. (** Division is left apart, since many different flavours are available *) diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index 0241c34762..8ea0122506 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -18,49 +18,6 @@ Module Type ZPowProp Include NZPowProp A A B. -(** Many results are directly the same as in NZPow, hence - the Include above. We extend nonetheless a few of them, - and add some results concerning negative first arg. -*) - -Lemma pow_mul_l' : forall a b c, (a*b)^c == a^c * b^c. -Proof. - intros a b c. destruct (le_gt_cases 0 c). now apply pow_mul_l. - rewrite !pow_neg by trivial. now nzsimpl. -Qed. - -Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b. -Proof. - intros a b Ha. destruct (le_gt_cases 0 b). - now apply pow_nonneg_nonneg. - rewrite !pow_neg by trivial. order. -Qed. - -Lemma pow_le_mono_l' : forall a b c, 0<=a<=b -> a^c <= b^c. -Proof. - intros a b c. destruct (le_gt_cases 0 c). now apply pow_le_mono_l. - rewrite !pow_neg by trivial. order. -Qed. - -(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *) - -Lemma pow_le_mono_r' : forall a b c, 0<a -> b<=c -> a^b <= a^c. -Proof. - intros a b c. destruct (le_gt_cases 0 b). - intros. apply pow_le_mono_r; try split; trivial. - rewrite !pow_neg by trivial. - intros. apply pow_nonneg. order. -Qed. - -Lemma pow_le_mono' : forall a b c d, 0<a<=c -> b<=d -> - a^b <= c^d. -Proof. - intros a b c d. destruct (le_gt_cases 0 b). - intros. apply pow_le_mono. trivial. split; trivial. - rewrite !pow_neg by trivial. - intros. apply pow_nonneg. intuition order. -Qed. - (** Parity of power *) Lemma even_pow : forall a b, 0<b -> even (a^b) = even a. @@ -86,7 +43,7 @@ Proof. rewrite 2 pow_2_r. now rewrite mul_opp_opp. assert (2*c < 0) by (apply mul_pos_neg; order'). - now rewrite !pow_neg. + now rewrite !pow_neg_r. Qed. Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b). @@ -98,7 +55,7 @@ Proof. rewrite pow_opp_even by (now exists c). apply mul_opp_l. apply double_above in GT. rewrite mul_0_r in GT. - rewrite !pow_neg by trivial. now rewrite opp_0. + rewrite !pow_neg_r by trivial. now rewrite opp_0. Qed. Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b. @@ -126,7 +83,7 @@ Proof. assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0). order. - now rewrite pow_neg. + now rewrite pow_neg_r. rewrite abs_neq by order. rewrite pow_opp_odd; trivial. now rewrite mul_opp_opp, mul_1_l. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index ee75e4aa18..48d166c0ab 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -39,7 +39,7 @@ Proof. rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc. Qed. -Lemma Zpow_neg : forall a b, b<0 -> Zpow a b = 0. +Lemma Zpow_neg_r : forall a b, b<0 -> Zpow a b = 0. Proof. now destruct b. Qed. @@ -171,7 +171,7 @@ Program Instance pow_wd : Proper (eq==>eq==>eq) Zpow. Definition pow_0_r := Zpow_0_r. Definition pow_succ_r := Zpow_succ_r. -Definition pow_neg := Zpow_neg. +Definition pow_neg_r := Zpow_neg_r. Definition pow := Zpow. (** Sqrt *) diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index d632d22607..c2965016ad 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -261,7 +261,7 @@ Proof. simpl. unfold Zpower_pos; simpl. ring. Qed. -Lemma pow_neg : forall a b, b<0 -> a^b == 0. +Lemma pow_neg_r : forall a b, b<0 -> a^b == 0. Proof. intros a b. zify. intros Hb. destruct [b]; reflexivity || discriminate. |