diff options
Diffstat (limited to 'theories')
| -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 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPow.v | 54 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 76 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSqrt.v | 25 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 12 |
11 files changed, 126 insertions, 124 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 4f88008be..6e6cd7f0f 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 0241c3476..8ea012250 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 ee75e4aa1..48d166c0a 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 d632d2260..c2965016a 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. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index ea1f1bad6..db6e86ea7 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -26,8 +26,13 @@ Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A). Declare Instance pow_wd : Proper (eq==>eq==>eq) pow. Axiom pow_0_r : forall a, a^0 == 1. Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. + Axiom pow_neg_r : forall a b, b<0 -> a^b == 0. End NZPowSpec. +(** The above [pow_neg_r] specification is useless (and trivially + provable) for N. Having it here allows to already derive + some slightly more general statements. *) + Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A. Module Type NZPow' (A : NZOrdAxiomsSig) := Pow' A <+ NZPowSpec A. @@ -83,10 +88,13 @@ Proof. now apply add_nonneg_nonneg. Qed. -Lemma pow_mul_l : forall a b c, 0<=c -> +Lemma pow_mul_l : forall a b c, (a*b)^c == a^c * b^c. Proof. - intros a b c Hc. apply le_ind with (4:=Hc). solve_predicate_wd. + intros a b c. + destruct (lt_ge_cases c 0) as [Hc|Hc]. + rewrite !(pow_neg_r _ _ Hc). now nzsimpl. + apply le_ind with (4:=Hc). solve_predicate_wd. now nzsimpl. clear c Hc. intros c Hc IH. nzsimpl; trivial. @@ -106,9 +114,12 @@ Qed. (** Positivity *) -Lemma pow_nonneg_nonneg : forall a b, 0<=a -> 0<=b -> 0<=a^b. +Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b. Proof. - intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + intros a b Ha. + destruct (lt_ge_cases b 0) as [Hb|Hb]. + now rewrite !(pow_neg_r _ _ Hb). + apply le_ind with (4:=Hb). solve_predicate_wd. nzsimpl; order'. clear b Hb. intros b Hb IH. nzsimpl; trivial. now apply mul_nonneg_nonneg. @@ -131,23 +142,28 @@ Proof. clear c Hc. intros c Hc IH (Ha,H). nzsimpl; try order. apply mul_lt_mono_nonneg; trivial. - apply pow_nonneg_nonneg; try order. + apply pow_nonneg; try order. apply IH. now split. Qed. -Lemma pow_le_mono_l : forall a b c, 0<=c -> 0<=a<=b -> a^c <= b^c. +Lemma pow_le_mono_l : forall a b c, 0<=a<=b -> a^c <= b^c. Proof. - intros a b c Hc (Ha,H). - apply lt_eq_cases in Hc; destruct Hc as [Hc|Hc]; [|rewrite <- Hc]. + intros a b c (Ha,H). + destruct (lt_trichotomy c 0) as [Hc|[Hc|Hc]]. + rewrite !(pow_neg_r _ _ Hc); now nzsimpl. + rewrite Hc; now nzsimpl. apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H]. apply lt_le_incl, pow_lt_mono_l; now try split. - now nzsimpl. Qed. -Lemma pow_gt_1 : forall a b, 1<a -> 0<b -> 1<a^b. +Lemma pow_gt_1 : forall a b, 1<a -> (0<b <-> 1<a^b). Proof. - intros a b Ha Hb. rewrite <- (pow_1_l b) by order. + intros a b Ha. split; intros Hb. + rewrite <- (pow_1_l b) by order. apply pow_lt_mono_l; try split; order'. + destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial. + rewrite pow_neg_r in Hb; order'. + rewrite H, pow_0_r in Hb. order. Qed. Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=b<c -> a^b < a^c. @@ -165,9 +181,11 @@ 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 -> 0<=b<=c -> a^b <= a^c. +Lemma pow_le_mono_r : forall a b c, 0<a -> b<=c -> a^b <= a^c. Proof. - intros a b c Ha (Hb,H). + intros a b c Ha H. + destruct (lt_ge_cases b 0) as [Hb|Hb]. + rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order. apply le_succ_l in Ha; rewrite <- one_succ in Ha. apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. @@ -175,7 +193,7 @@ Proof. nzsimpl; order. Qed. -Lemma pow_le_mono : forall a b c d, 0<a<=c -> 0<=b<=d -> +Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d -> a^b <= c^d. Proof. intros. transitivity (a^d). @@ -237,7 +255,7 @@ Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> Proof. intros a b c Ha Hb Hc. split; intro LE. - apply pow_le_mono_l; try split; trivial. order. + apply pow_le_mono_l; try split; trivial. destruct (le_gt_cases a b) as [LE'|GT]; trivial. assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). order. @@ -299,10 +317,10 @@ Proof. apply add_le_mono. rewrite <- add_0_r at 1. apply add_le_mono_l. apply mul_nonneg_nonneg; trivial. - apply pow_nonneg_nonneg; trivial. + apply pow_nonneg; trivial. rewrite <- add_0_l at 1. apply add_le_mono_r. apply mul_nonneg_nonneg; trivial. - apply pow_nonneg_nonneg; trivial. + apply pow_nonneg; trivial. apply mul_le_mono_nonneg_l; trivial. now apply add_nonneg_nonneg. Qed. @@ -343,7 +361,7 @@ Proof. assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order). rewrite EQ', <- !mul_assoc. apply mul_le_mono_nonneg_l. - apply pow_nonneg_nonneg; order'. + apply pow_nonneg; order'. destruct (le_gt_cases a b). apply aux; try split; order'. rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)). diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index a40aa7657..d84748ee2 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -25,6 +25,7 @@ Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A. Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A). Declare Instance sqrt_wd : Proper (eq==>eq) sqrt. Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a). + Axiom sqrt_neg : forall a, a<0 -> √a == 0. End NZSqrtSpec. Module Type NZSqrt (A : NZOrdAxiomsSig) := Sqrt A <+ NZSqrtSpec A. @@ -39,10 +40,10 @@ Module Type NZSqrtProp (** First, sqrt is non-negative *) -Lemma sqrt_spec_nonneg : forall a b, 0<=a -> +Lemma sqrt_spec_nonneg : forall a b, b*b <= a < S b * S b -> 0 <= b. Proof. - intros a b Ha (LE,LT). + intros a b (LE,LT). destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso. assert (S b * S b < b * b). rewrite mul_succ_l, <- (add_0_r (b*b)). @@ -52,18 +53,21 @@ Proof. order. Qed. -Lemma sqrt_nonneg : forall a, 0<=a -> 0<=√a. +Lemma sqrt_nonneg : forall a, 0<=√a. Proof. - intros. now apply (sqrt_spec_nonneg a), sqrt_spec. + intros. destruct (lt_ge_cases a 0) as [Ha|Ha]. + now rewrite (sqrt_neg _ Ha). + now apply (sqrt_spec_nonneg a), sqrt_spec. Qed. (** The spec of sqrt indeed determines it *) -Lemma sqrt_unique : forall a b, 0<=a -> b*b<=a<(S b)*(S b) -> √a == b. +Lemma sqrt_unique : forall a b, b*b <= a < S b * S b -> √a == b. Proof. - intros a b Ha (LEb,LTb). - assert (0<=b) by (apply (sqrt_spec_nonneg a); try split; trivial). - assert (0<=√a) by now apply sqrt_nonneg. + intros a b (LEb,LTb). + assert (Ha : 0<=a) by (transitivity (b*b); trivial using square_nonneg). + assert (Hb : 0<=b) by (apply (sqrt_spec_nonneg a); now split). + assert (Ha': 0<=√a) by now apply sqrt_nonneg. destruct (sqrt_spec a Ha) as (LEa,LTa). assert (b <= √a). apply lt_succ_r, square_lt_simpl_nonneg; [|order]. @@ -80,16 +84,17 @@ Lemma sqrt_square : forall a, 0<=a -> √(a*a) == a. Proof. intros a Ha. apply sqrt_unique. - apply square_nonneg. split. order. apply mul_lt_mono_nonneg; trivial using lt_succ_diag_r. Qed. (** Sqrt is a monotone function (but not a strict one) *) -Lemma sqrt_le_mono : forall a b, 0<=a<=b -> √a <= √b. +Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b. Proof. - intros a b (Ha,Hab). + intros a b Hab. + destruct (lt_ge_cases a 0) as [Ha|Ha]. + rewrite (sqrt_neg _ Ha). apply sqrt_nonneg. assert (Hb : 0 <= b) by order. destruct (sqrt_spec a Ha) as (LE,_). destruct (sqrt_spec b Hb) as (_,LT). @@ -100,9 +105,12 @@ Qed. (** No reverse result for <=, consider for instance √2 <= √1 *) -Lemma sqrt_lt_cancel : forall a b, 0<=a -> 0<=b -> √a < √b -> a < b. +Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b. Proof. - intros a b Ha Hb H. + intros a b H. + destruct (lt_ge_cases b 0) as [Hb|Hb]. + rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order. + destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|]. destruct (sqrt_spec a Ha) as (_,LT). destruct (sqrt_spec b Hb) as (LE,_). apply le_succ_l in H. @@ -119,7 +127,7 @@ Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b*b<=a <-> b <= √a). Proof. intros a b Ha Hb. split; intros H. rewrite <- (sqrt_square b); trivial. - apply sqrt_le_mono. split. apply square_nonneg. trivial. + now apply sqrt_le_mono. destruct (sqrt_spec a Ha) as (LE,LT). transitivity (√a * √a); trivial. now apply mul_le_mono_nonneg. @@ -133,8 +141,7 @@ Proof. destruct (sqrt_spec a Ha) as (LE,_). apply square_lt_simpl_nonneg; try order. rewrite <- (sqrt_square b Hb) in H. - apply sqrt_lt_cancel; trivial. - apply square_nonneg. + now apply sqrt_lt_cancel. Qed. (** Sqrt and basic constants *) @@ -151,7 +158,7 @@ Qed. Lemma sqrt_2 : √2 == 1. Proof. - apply sqrt_unique. order'. nzsimpl. split. order'. + apply sqrt_unique. nzsimpl. split. order'. apply lt_succ_r, lt_le_incl, lt_succ_r. nzsimpl'; order. Qed. @@ -178,11 +185,15 @@ Qed. (** Due to rounding error, we don't have the usual √(a*b) = √a*√b but only lower and upper bounds. *) -Lemma sqrt_mul_below : forall a b, 0<=a -> 0<=b -> √a * √b <= √(a*b). +Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b). Proof. - intros a b Ha Hb. - assert (Ha':=sqrt_nonneg _ Ha). - assert (Hb':=sqrt_nonneg _ Hb). + intros a b. + destruct (lt_ge_cases a 0) as [Ha|Ha]. + rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg. + destruct (lt_ge_cases b 0) as [Hb|Hb]. + rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg. + assert (Ha':=sqrt_nonneg a). + assert (Hb':=sqrt_nonneg b). apply sqrt_le_square; try now apply mul_nonneg_nonneg. rewrite mul_shuffle1. apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg. @@ -190,8 +201,7 @@ Proof. now apply sqrt_spec. Qed. -Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> - √(a*b) < S (√a) * S (√b). +Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b). Proof. intros a b Ha Hb. apply sqrt_lt_square. @@ -211,11 +221,19 @@ Qed. (** Sqrt and addition *) -Lemma sqrt_add_le : forall a b, 0<=a -> 0<=b -> √(a+b) <= √a + √b. +Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b. Proof. - intros a b Ha Hb. - assert (Ha':=sqrt_nonneg _ Ha). - assert (Hb':=sqrt_nonneg _ Hb). + assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b). + intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl. + apply sqrt_le_mono. + rewrite <- (add_0_l b) at 2. + apply add_le_mono_r; order. + intros a b. + destruct (lt_ge_cases a 0) as [Ha|Ha]. now apply AUX. + destruct (lt_ge_cases b 0) as [Hb|Hb]. + rewrite (add_comm a), (add_comm (√a)); now apply AUX. + assert (Ha':=sqrt_nonneg a). + assert (Hb':=sqrt_nonneg b). rewrite <- lt_succ_r. apply sqrt_lt_square. now apply add_nonneg_nonneg. @@ -241,8 +259,8 @@ Qed. Lemma add_sqrt_le : forall a b, 0<=a -> 0<=b -> √a + √b <= √(2*(a+b)). Proof. intros a b Ha Hb. - assert (Ha':=sqrt_nonneg _ Ha). - assert (Hb':=sqrt_nonneg _ Hb). + assert (Ha':=sqrt_nonneg a). + assert (Hb':=sqrt_nonneg b). apply sqrt_le_square. apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg. now apply add_nonneg_nonneg. diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v index 92e90b9c8..4a9cf536b 100644 --- a/theories/Numbers/Natural/Abstract/NSqrt.v +++ b/theories/Numbers/Natural/Abstract/NSqrt.v @@ -22,17 +22,17 @@ Module NSqrtProp (Import A : NAxiomsSig')(Import B : NSubProp A). Lemma sqrt_spec' : forall a, √a*√a <= a < S (√a) * S (√a). Proof. wrap sqrt_spec. Qed. -Lemma sqrt_unique : forall a b, b*b<=a<(S b)*(S b) -> √a == b. -Proof. wrap sqrt_unique. Qed. +Definition sqrt_unique : forall a b, b*b<=a<(S b)*(S b) -> √a == b + := sqrt_unique. Lemma sqrt_square : forall a, √(a*a) == a. Proof. wrap sqrt_square. Qed. -Lemma sqrt_le_mono : forall a b, a<=b -> √a <= √b. -Proof. wrap sqrt_le_mono. Qed. +Definition sqrt_le_mono : forall a b, a<=b -> √a <= √b + := sqrt_le_mono. -Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b. -Proof. wrap sqrt_lt_cancel. Qed. +Definition sqrt_lt_cancel : forall a b, √a < √b -> a < b + := sqrt_lt_cancel. Lemma sqrt_le_square : forall a b, b*b<=a <-> b <= √a. Proof. wrap sqrt_le_square. Qed. @@ -44,19 +44,20 @@ Definition sqrt_0 := sqrt_0. Definition sqrt_1 := sqrt_1. Definition sqrt_2 := sqrt_2. -Definition sqrt_lt_lin : forall a, 1<a -> √a<a := sqrt_lt_lin. +Definition sqrt_lt_lin : forall a, 1<a -> √a<a + := sqrt_lt_lin. -Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a. +Lemma sqrt_le_lin : forall a, √a<=a. Proof. wrap sqrt_le_lin. Qed. -Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b). -Proof. wrap sqrt_mul_below. Qed. +Definition sqrt_mul_below : forall a b, √a * √b <= √(a*b) + := sqrt_mul_below. Lemma sqrt_mul_above : forall a b, √(a*b) < S (√a) * S (√b). Proof. wrap sqrt_mul_above. Qed. -Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b. -Proof. wrap sqrt_add_le. Qed. +Definition sqrt_add_le : forall a b, √(a+b) <= √a + √b + := sqrt_add_le. Lemma add_sqrt_le : forall a b, √a + √b <= √(2*(a+b)). Proof. wrap add_sqrt_le. Qed. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index ec0fa89bf..60a836d41 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -746,7 +746,7 @@ Module Make (W0:CyclicType) <: NType. Theorem spec_sqrt: forall x, [sqrt x] = Zsqrt [x]. Proof. intros x. - symmetry. apply Z.sqrt_unique. apply spec_pos. + symmetry. apply Z.sqrt_unique. rewrite <- ! Zpower_2. apply spec_sqrt_aux. Qed. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 348eee5ed..8b7b06966 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -163,14 +163,18 @@ Definition odd_spec := Nodd_spec. (** Power *) +Program Instance pow_wd : Proper (eq==>eq==>eq) Npow. Definition pow_0_r := Npow_0_r. Definition pow_succ_r n p (H:0 <= p) := Npow_succ_r n p. -Program Instance pow_wd : Proper (eq==>eq==>eq) Npow. +Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. +Proof. destruct b; discriminate. Qed. (** Sqrt *) Program Instance sqrt_wd : Proper (eq==>eq) Nsqrt. Definition sqrt_spec n (H:0<=n) := Nsqrt_spec n. +Lemma sqrt_neg : forall a, a<0 -> Nsqrt a = 0. +Proof. destruct a; discriminate. Qed. (** The instantiation of operations. Placing them at the very end avoids having indirections in above lemmas. *) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index b91b43e31..de5ef4787 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -369,10 +369,12 @@ Definition odd_spec := odd_spec. Program Instance pow_wd : Proper (eq==>eq==>eq) pow. Definition pow_0_r := pow_0_r. Definition pow_succ_r := pow_succ_r. +Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed. Definition pow := pow. -Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a. Program Instance sqrt_wd : Proper (eq==>eq) sqrt. +Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a. +Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed. Definition sqrt := sqrt. Definition div := div. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index f072fc24a..f242951e5 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -204,6 +204,12 @@ Proof. simpl. unfold Zpower_pos; simpl. ring. Qed. +Lemma pow_neg_r : forall a b, b<0 -> a^b == 0. +Proof. + intros a b. zify. intro Hb. exfalso. + generalize (spec_pos b); omega. +Qed. + Lemma pow_pow_N : forall a b, a^b == pow_N a (to_N b). Proof. intros. zify. f_equal. @@ -230,6 +236,12 @@ Proof. intros n. zify. apply Zsqrt_spec. Qed. +Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0. +Proof. + intros n. zify. intro H. exfalso. + generalize (spec_pos n); omega. +Qed. + (** Even / Odd *) Definition Even n := exists m, n == 2*m. |