diff options
Diffstat (limited to 'theories/Numbers')
20 files changed, 550 insertions, 62 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 6fcb4cf910..2d9eb395a6 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -574,27 +574,19 @@ Section ZModulo. generalize (Z_mod_lt [|x|] 2); omega. Qed. - Definition sqrt x := Zsqrt_plain [|x|]. + Definition sqrt x := Zsqrt [|x|]. Lemma spec_sqrt : forall x, [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. Proof. intros. unfold sqrt. repeat rewrite Zpower_2. - replace [|Zsqrt_plain [|x|]|] with (Zsqrt_plain [|x|]). - apply Zsqrt_interval; auto with zarith. + replace [|Zsqrt [|x|]|] with (Zsqrt [|x|]). + apply Zsqrt_spec; auto with zarith. symmetry; apply Zmod_small. - split. - apply Zsqrt_plain_is_pos; auto with zarith. - - cut (Zsqrt_plain [|x|] <= (wB-1)); try omega. - rewrite <- (Zsqrt_square_id (wB-1)). - apply Zsqrt_le. - split; auto. - apply Zle_trans with (wB-1); auto with zarith. - generalize (spec_to_Z x); auto with zarith. - apply Zsquare_le. - generalize wB_pos; auto with zarith. + split. apply Z.sqrt_nonneg; auto. + apply Zle_lt_trans with [|x|]; auto. + apply Z.sqrt_le_lin; auto. Qed. Definition sqrt2 x y := @@ -602,7 +594,7 @@ Section ZModulo. match z with | Z0 => (0, C0 0) | Zpos p => - let (s,r,_,_) := sqrtrempos p in + let (s,r) := Zsqrtrem (Zpos p) in (s, if Z_lt_le_dec r wB then C0 r else C1 (r-wB)) | Zneg _ => (0, C0 0) end. @@ -618,11 +610,12 @@ Section ZModulo. remember ([|x|]*wB+[|y|]) as z. destruct z. auto with zarith. - destruct sqrtrempos; intros. + generalize (Zsqrtrem_spec (Zpos p)). + destruct Zsqrtrem as (s,r); intros [U V]; auto with zarith. assert (s < wB). destruct (Z_lt_le_dec s wB); auto. assert (wB * wB <= Zpos p). - rewrite e. + rewrite U. apply Zle_trans with (s*s); try omega. apply Zmult_le_compat; generalize wB_pos; auto with zarith. assert (Zpos p < wB*wB). diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 38855a85da..4f88008be4 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -9,7 +9,7 @@ (************************************************************************) Require Export NZAxioms. -Require Import NZPow. +Require Import NZPow NZSqrt. (** We obtain integers by postulating that successor of predecessor is identity. *) @@ -76,15 +76,20 @@ 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. (** Let's group everything *) Module Type ZAxiomsSig := ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow <+ ZPowSpecNeg. + <+ NZPow.NZPow <+ ZPowSpecNeg <+ NZSqrt.NZSqrt <+ ZSqrtSpecNeg. Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow' <+ ZPowSpecNeg. + <+ NZPow.NZPow' <+ ZPowSpecNeg <+ NZSqrt.NZSqrt' <+ ZSqrtSpecNeg. (** Division is left apart, since many different flavours are available *) diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 25989b2d40..1010a0f2fb 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -92,14 +92,7 @@ Qed. Notation mul_nonpos := le_mul_0 (only parsing). -Theorem le_0_square : forall n, 0 <= n * n. -Proof. -intro n; destruct (neg_nonneg_cases n). -apply lt_le_incl; now apply mul_neg_neg. -now apply mul_nonneg_nonneg. -Qed. - -Notation square_nonneg := le_0_square (only parsing). +Notation le_0_square := square_nonneg (only parsing). Theorem nlt_square_0 : forall n, ~ n * n < 0. Proof. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 7b9c6f4528..8b34e5b2db 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -11,6 +11,5 @@ Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow. (** This functor summarizes all known facts about Z. *) Module Type ZProp (Z:ZAxiomsSig) := - ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z. - - + ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z + <+ NZSqrt.NZSqrtProp Z Z. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index f9490cc9c7..099554cd0b 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -338,15 +338,14 @@ Module Make (N:NType) <: ZType. | Neg nx => Neg N.zero end. - Theorem spec_sqrt: forall x, 0 <= to_Z x -> - to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. + Theorem spec_sqrt: forall x, to_Z (sqrt x) = Zsqrt (to_Z x). Proof. - unfold to_Z, sqrt; intros [x | x] H. - exact (N.spec_sqrt x). - replace (N.to_Z x) with 0. - rewrite N.spec_0; simpl Zpower; unfold Zpower_pos, iter_pos; - auto with zarith. - generalize (N.spec_pos x); auto with zarith. + destruct x as [p|p]; simpl. + apply N.spec_sqrt. + rewrite N.spec_0. + destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ]. + rewrite Zsqrt_neg; auto with zarith. + now rewrite <- EQ. Qed. Definition div_eucl x y := diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 5f87283940..ee75e4aa18 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -10,7 +10,7 @@ Require Import ZAxioms ZProperties. -Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven. +Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven Zsqrt_def. Local Open Scope Z_scope. @@ -174,6 +174,17 @@ Definition pow_succ_r := Zpow_succ_r. Definition pow_neg := Zpow_neg. Definition pow := Zpow. +(** Sqrt *) + +(** NB : we use a new Zsqrt defined in Zsqrt_def, the previous + module Zsqrt.v is now Zsqrt_compat.v *) + +Program Instance sqrt_wd : Proper (eq==>eq) Zsqrt. + +Definition sqrt_spec := Zsqrt_spec. +Definition sqrt_neg := Zsqrt_neg. +Definition sqrt := Zsqrt. + (** We define [eq] only here to avoid refering to this [eq] above. *) Definition eq := (@eq Z). diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index be201f2d66..37f5b294e1 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -78,13 +78,12 @@ Module Type ZType. Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n. Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n. Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n]. - Parameter spec_sqrt: forall x, 0 <= [x] -> - [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x]. Parameter spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. Parameter spec_div: forall x y, [div x y] = [x] / [y]. Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y]. - Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b]. Parameter spec_sgn : forall x, [sgn x] = Zsgn [x]. Parameter spec_abs : forall x, [abs x] = Zabs [x]. Parameter spec_even : forall x, even x = Zeven_bool [x]. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 3e63755434..d632d22607 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -18,7 +18,7 @@ Module ZTypeIsZAxioms (Import Z : ZType'). Hint Rewrite spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ - spec_mul spec_opp spec_of_Z spec_div spec_modulo + spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn spec_pow spec_even spec_odd : zsimpl. @@ -278,6 +278,21 @@ Proof. intros a b. red. now rewrite spec_pow_N, spec_pow_pos. Qed. +(** Sqrt *) + +Program Instance sqrt_wd : Proper (eq==>eq) sqrt. + +Lemma sqrt_spec : forall n, 0<=n -> + (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)). +Proof. + intros n. zify. apply Zsqrt_spec. +Qed. + +Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0. +Proof. + intros n. zify. apply Zsqrt_neg. +Qed. + (** Even / Odd *) Definition Even n := exists m, n == 2*m. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 530044ab0b..8f1b8cb6e9 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -295,11 +295,60 @@ assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonneg. apply -> lt_nge in F. false_hyp H2 F. Qed. -Theorem mul_2_mono_l : forall n m, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m. Proof. -intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m (1 + 1)). -rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l. -apply add_pos_pos; now apply lt_0_1. +intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m two). +rewrite two_succ. nzsimpl. now rewrite le_succ_l. +order'. +Qed. + +(** A few results about squares *) + +Lemma square_nonneg : forall a, 0 <= a * a. +Proof. + intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). + now apply mul_le_mono_nonpos_l. + apply mul_le_mono_nonneg_l; order. +Qed. + +Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b*a+a*b <= a*a+b*b. +Proof. + assert (AUX : forall a b, 0<=a<=b -> b*a+a*b <= a*a+b*b). + intros a b (Ha,H). + destruct (le_exists_sub _ _ H) as (d & EQ & Hd). + rewrite EQ. + rewrite 2 mul_add_distr_r. + rewrite !add_assoc. apply add_le_mono_r. + rewrite add_comm. apply add_le_mono_l. + apply mul_le_mono_nonneg_l; trivial. order. + intros a b Ha Hb. + destruct (le_gt_cases a b). + apply AUX; split; order. + rewrite (add_comm (b*a)), (add_comm (a*a)). + apply AUX; split; order. +Qed. + +Lemma add_square_le : forall a b, 0<=a -> 0<=b -> + a*a + b*b <= (a+b)*(a+b). +Proof. + intros a b Ha Hb. + rewrite mul_add_distr_r, !mul_add_distr_l. + rewrite add_assoc. + apply add_le_mono_r. + rewrite <- add_assoc. + rewrite <- (add_0_r (a*a)) at 1. + apply add_le_mono_l. + apply add_nonneg_nonneg; now apply mul_nonneg_nonneg. +Qed. + +Lemma square_add_le : forall a b, 0<=a -> 0<=b -> + (a+b)*(a+b) <= 2*(a*a + b*b). +Proof. + intros a b Ha Hb. + rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'. + rewrite <- !add_assoc. apply add_le_mono_l. + rewrite !add_assoc. apply add_le_mono_r. + apply crossmul_le_addsquare; order. Qed. End NZMulOrderProp. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index e2e3980257..ef9057c068 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -239,9 +239,14 @@ Proof. apply lt_le_incl, lt_0_1. Qed. +Theorem lt_1_2 : 1 < 2. +Proof. +rewrite two_succ. apply lt_succ_diag_r. +Qed. + Theorem lt_0_2 : 0 < 2. Proof. -transitivity 1. apply lt_0_1. rewrite two_succ. apply lt_succ_diag_r. +transitivity 1. apply lt_0_1. apply lt_1_2. Qed. Theorem le_0_2 : 0 <= 2. @@ -256,7 +261,7 @@ Qed. (** The order tactic enriched with some knowledge of 0,1,2 *) -Ltac order' := generalize lt_0_1 lt_0_2; order. +Ltac order' := generalize lt_0_1 lt_1_2; order. (** More Trichotomy, decidability and double negation elimination. *) diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v new file mode 100644 index 0000000000..425e4d6b89 --- /dev/null +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -0,0 +1,255 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Square Root Function *) + +Require Import NZAxioms NZMulOrder. + +(** Interface of a sqrt function, then its specification on naturals *) + +Module Type Sqrt (Import T:Typ). + Parameters Inline sqrt : t -> t. +End Sqrt. + +Module Type SqrtNotation (T:Typ)(Import NZ:Sqrt T). + Notation "√ x" := (sqrt x) (at level 25). +End SqrtNotation. + +Module Type Sqrt' (T:Typ) := Sqrt T <+ SqrtNotation T. + +Module Type NZSqrtSpec (Import NZ : NZOrdAxiomsSig')(Import P : Sqrt' NZ). + Declare Instance sqrt_wd : Proper (eq==>eq) sqrt. + Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a). +End NZSqrtSpec. + +Module Type NZSqrt (NZ:NZOrdAxiomsSig) := Sqrt NZ <+ NZSqrtSpec NZ. +Module Type NZSqrt' (NZ:NZOrdAxiomsSig) := Sqrt' NZ <+ NZSqrtSpec NZ. + +(** Derived properties of power *) + +Module NZSqrtProp + (Import NZ : NZOrdAxiomsSig') + (Import NZP' : NZSqrt' NZ) + (Import NZP : NZMulOrderProp NZ). + +(** First, sqrt is non-negative *) + +Lemma sqrt_spec_nonneg : forall a b, 0<=a -> + b*b <= a < S b * S b -> 0 <= b. +Proof. + intros a b Ha (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)). + apply add_lt_le_mono. + apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r. + now apply le_succ_l. + order. +Qed. + +Lemma sqrt_nonneg : forall a, 0<=a -> 0<=√a. +Proof. + intros. 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. +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. + destruct (sqrt_spec a Ha) as (LEa,LTa). + assert (b <= √a). + apply lt_succ_r, square_lt_simpl_nonneg; [|order]. + now apply lt_le_incl, lt_succ_r. + assert (√a <= b). + apply lt_succ_r, square_lt_simpl_nonneg; [|order]. + now apply lt_le_incl, lt_succ_r. + order. +Qed. + +(** Sqrt is exact on squares *) + +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. +Proof. + intros a b (Ha,Hab). + assert (Hb : 0 <= b) by order. + destruct (sqrt_spec a Ha) as (LE,_). + destruct (sqrt_spec b Hb) as (_,LT). + apply lt_succ_r. + apply square_lt_simpl_nonneg; try order. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. +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. +Proof. + intros a b Ha Hb H. + destruct (sqrt_spec a Ha) as (_,LT). + destruct (sqrt_spec b Hb) as (LE,_). + apply le_succ_l in H. + assert (S (√a) * S (√a) <= √b * √b). + apply mul_le_mono_nonneg; trivial. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + order. +Qed. + +(** When left side is a square, we have an equivalence for <= *) + +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. + destruct (sqrt_spec a Ha) as (LE,LT). + transitivity (√a * √a); trivial. + now apply mul_le_mono_nonneg. +Qed. + +(** When right side is a square, we have an equivalence for < *) + +Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b*b <-> √a < b). +Proof. + intros a b Ha Hb. split; intros H. + 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. +Qed. + +(** Sqrt and basic constants *) + +Lemma sqrt_0 : √0 == 0. +Proof. + rewrite <- (mul_0_l 0) at 1. now apply sqrt_square. +Qed. + +Lemma sqrt_1 : √1 == 1. +Proof. + rewrite <- (mul_1_l 1) at 1. apply sqrt_square. order'. +Qed. + +Lemma sqrt_2 : √2 == 1. +Proof. + apply sqrt_unique. order'. nzsimpl. split. order'. + apply lt_succ_r, lt_le_incl, lt_succ_r. nzsimpl'; order. +Qed. + +Lemma sqrt_lt_lin : forall a, 1<a -> √a<a. +Proof. + intros a Ha. rewrite <- sqrt_lt_square; try order'. + rewrite <- (mul_1_r a) at 1. + rewrite <- mul_lt_mono_pos_l; order'. +Qed. + +Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a. +Proof. + intros a Ha. + destruct (le_gt_cases a 0) as [H|H]. + setoid_replace a with 0 by order. now rewrite sqrt_0. + destruct (le_gt_cases a 1) as [H'|H']. + rewrite <- le_succ_l, <- one_succ in H. + setoid_replace a with 1 by order. now rewrite sqrt_1. + now apply lt_le_incl, sqrt_lt_lin. +Qed. + +(** Sqrt and multiplication. *) + +(** 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). +Proof. + intros a b Ha Hb. + assert (Ha':=sqrt_nonneg _ Ha). + assert (Hb':=sqrt_nonneg _ Hb). + apply sqrt_le_square; try now apply mul_nonneg_nonneg. + rewrite mul_shuffle1. + apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg. + now apply sqrt_spec. + now apply sqrt_spec. +Qed. + +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. + now apply mul_nonneg_nonneg. + apply mul_nonneg_nonneg. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + rewrite mul_shuffle1. + apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec. +Qed. + +(** And we can't find better approximations in general. + - The lower bound is exact for squares + - Concerning the upper bound, for any c>0, take a=b=c*c-1, + then √(a*b) = c*c -1 while S √a = S √b = c +*) + +(** Sqrt and addition *) + +Lemma sqrt_add_le : forall a b, 0<=a -> 0<=b -> √(a+b) <= √a + √b. +Proof. + intros a b Ha Hb. + assert (Ha':=sqrt_nonneg _ Ha). + assert (Hb':=sqrt_nonneg _ Hb). + rewrite <- lt_succ_r. + apply sqrt_lt_square. + now apply add_nonneg_nonneg. + now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg. + destruct (sqrt_spec a Ha) as (_,LTa). + destruct (sqrt_spec b Hb) as (_,LTb). + revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r. + intros LTa LTb. + assert (H:=add_le_mono _ _ _ _ LTa LTb). + etransitivity; [eexact H|]. clear LTa LTb H. + rewrite <- (add_assoc _ (√a) (√a)). + rewrite <- (add_assoc _ (√b) (√b)). + rewrite add_shuffle1. + rewrite <- (add_assoc _ (√a + √b)). + rewrite (add_shuffle1 (√a) (√b)). + apply add_le_mono_r. + now apply add_square_le. +Qed. + +(** convexity inequality for sqrt: sqrt of middle is above middle + of square roots. *) + +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). + apply sqrt_le_square. + apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg. + now apply add_nonneg_nonneg. + transitivity (2*(√a*√a + √b*√b)). + now apply square_add_le. + apply mul_le_mono_nonneg_l. order'. + apply add_le_mono; now apply sqrt_spec. +Qed. + +End NZSqrtProp. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 66ff2ded54..b360c016f3 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Export NZAxioms NZPow NZDiv. +Require Export NZAxioms NZPow NZSqrt NZDiv. (** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *) @@ -32,7 +32,7 @@ Module Type Parity (Import N : NAxiomsMiniSig'). Axiom odd_spec : forall n, odd n = true <-> Odd n. End Parity. -(** Power function : NZPow is enough *) +(** For Power and Sqrt functions : NZPow and NZSqrt are enough *) (** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon, and add to that a N-specific constraint. *) @@ -45,10 +45,12 @@ End NDivSpecific. (** We now group everything together. *) Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity - <+ NZPow.NZPow <+ DivMod <+ NZDivCommon <+ NDivSpecific. + <+ NZPow.NZPow <+ NZSqrt.NZSqrt + <+ DivMod <+ NZDivCommon <+ NDivSpecific. Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity - <+ NZPow.NZPow' <+ DivMod' <+ NZDivCommon <+ NDivSpecific. + <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' + <+ DivMod' <+ NZDivCommon <+ NDivSpecific. (** It could also be interesting to have a constructive recursor function. *) diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index c1977f3533..fc8f27ddc9 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -7,9 +7,9 @@ (************************************************************************) Require Export NAxioms. -Require Import NMaxMin NParity NPow NDiv. +Require Import NMaxMin NParity NPow NSqrt NDiv. (** This functor summarizes all known facts about N. *) Module Type NProp (N:NAxiomsSig) := - NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NDivProp N. + NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N <+ NDivProp N. diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v new file mode 100644 index 0000000000..d5916bdc2d --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NSqrt.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Properties of Square Root Function *) + +Require Import NAxioms NSub NZSqrt. + +Module NSqrtProp (Import N : NAxiomsSig')(Import NS : NSubProp N). + + Module Import NZSqrtP := NZSqrtProp N N NS. + + Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l. + Ltac wrap l := intros; apply l; auto'. + + (** We redefine NZSqrt's results, without the non-negative hyps *) + +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. + +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. + +Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b. +Proof. wrap sqrt_lt_cancel. Qed. + +Lemma sqrt_le_square : forall a b, b*b<=a <-> b <= √a. +Proof. wrap sqrt_le_square. Qed. + +Lemma sqrt_lt_square : forall a b, a<b*b <-> √a < b. +Proof. wrap sqrt_lt_square. Qed. + +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. + +Lemma sqrt_le_lin : forall a, 0<=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. + +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. + +Lemma add_sqrt_le : forall a b, √a + √b <= √(2*(a+b)). +Proof. wrap add_sqrt_le. Qed. + +End NSqrtProp. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 9e6e4b6092..ec0fa89bff 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -738,11 +738,18 @@ Module Make (W0:CyclicType) <: NType. Lemma sqrt_fold : sqrt = iter_t sqrtn. Proof. red_t; reflexivity. Qed. - Theorem spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + Theorem spec_sqrt_aux: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. Proof. intros x. rewrite sqrt_fold. destr_t x as (n,x). exact (ZnZ.spec_sqrt x). Qed. + Theorem spec_sqrt: forall x, [sqrt x] = Zsqrt [x]. + Proof. + intros x. + symmetry. apply Z.sqrt_unique. apply spec_pos. + rewrite <- ! Zpower_2. apply spec_sqrt_aux. + Qed. + (** * Power *) Fixpoint pow_pos (x:t)(p:positive) : t := diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index d1217d407e..348eee5ed2 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import BinPos Ndiv_def. +Require Import BinPos Ndiv_def Nsqrt_def. Require Export BinNat. Require Import NAxioms NProperties. @@ -167,6 +167,11 @@ 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. +(** Sqrt *) + +Program Instance sqrt_wd : Proper (eq==>eq) Nsqrt. +Definition sqrt_spec n (H:0<=n) := Nsqrt_spec n. + (** The instantiation of operations. Placing them at the very end avoids having indirections in above lemmas. *) @@ -192,6 +197,7 @@ Definition modulo := Nmod. Definition pow := Npow. Definition even := Neven. Definition odd := Nodd. +Definition sqrt := Nsqrt. Include NProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index bbf4f5cd7b..b91b43e310 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import - Bool Peano Peano_dec Compare_dec Plus Minus Le EqNat NAxioms NProperties. + Bool Peano Peano_dec Compare_dec Plus Minus Le Lt EqNat NAxioms NProperties. (** Functions not already defined *) @@ -134,6 +134,75 @@ Proof. apply le_n_S, le_minus. Qed. +(** Square root *) + +(** The following square root function is linear (and tail-recursive). + With Peano representation, we can't do better. For faster algorithm, + see Psqrt/Zsqrt/Nsqrt... + + We search the square root of n = k + p^2 + (q - r) + with q = 2p and 0<=r<=q. We starts with p=q=r=0, hence + looking for the square root of n = k. Then we progressively + decrease k and r. When k = S k' and r=0, it means we can use (S p) + as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2. + When k reaches 0, we have found the biggest p^2 square contained + in n, hence the square root of n is p. +*) + +Fixpoint sqrt_iter k p q r := + match k with + | O => p + | S k' => match r with + | O => sqrt_iter k' (S p) (S (S q)) (S (S q)) + | S r' => sqrt_iter k' p q r' + end + end. + +Definition sqrt n := sqrt_iter n 0 0 0. + +Lemma sqrt_iter_spec : forall k p q r, + q = p+p -> r<=q -> + let s := sqrt_iter k p q r in + s*s <= k + p*p + (q - r) < (S s)*(S s). +Proof. + induction k. + (* k = 0 *) + simpl; intros p q r Hq Hr. + split. + apply le_plus_l. + apply le_lt_n_Sm. + rewrite <- mult_n_Sm. + rewrite plus_assoc, (plus_comm p), <- plus_assoc. + apply plus_le_compat; trivial. + rewrite <- Hq. apply le_minus. + (* k = S k' *) + destruct r. + (* r = 0 *) + intros Hq _. + replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))). + apply IHk. + simpl. rewrite <- plus_n_Sm. congruence. + auto with arith. + rewrite minus_diag, <- minus_n_O, <- plus_n_O. simpl. + rewrite <- plus_n_Sm; f_equal. rewrite <- plus_assoc; f_equal. + rewrite <- mult_n_Sm, (plus_comm p), <- plus_assoc. congruence. + (* r = S r' *) + intros Hq Hr. + replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)). + apply IHk; auto with arith. + simpl. rewrite plus_n_Sm. f_equal. rewrite minus_Sn_m; auto. +Qed. + +Lemma sqrt_spec : forall n, + let s := sqrt n in s*s <= n < S s * S s. +Proof. + intros. + replace n with (n + 0*0 + (0-0)). + apply sqrt_iter_spec; auto. + simpl. now rewrite <- 2 plus_n_O. +Qed. + + (** * Implementation of [NAxiomsSig] by [nat] *) Module Nat @@ -297,10 +366,14 @@ Definition odd := odd. Definition even_spec := even_spec. Definition odd_spec := odd_spec. -Definition pow := pow. Program Instance pow_wd : Proper (eq==>eq==>eq) pow. Definition pow_0_r := pow_0_r. Definition pow_succ_r := pow_succ_r. +Definition pow := pow. + +Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a. +Program Instance sqrt_wd : Proper (eq==>eq) sqrt. +Definition sqrt := sqrt. Definition div := div. Definition modulo := modulo. diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 7cf3e7046b..703897eba5 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -77,7 +77,7 @@ Module Type NType. Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n. Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n. Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n]. - Parameter spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x]. Parameter spec_log2_0: forall x, [x] = 0 -> [log2 x] = 0. Parameter spec_log2: forall x, [x]<>0 -> 2^[log2 x] <= [x] < 2^([log2 x]+1). Parameter spec_div_eucl: forall x y, diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index e1dc5349bc..f072fc24aa 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -1,4 +1,5 @@ (************************************************************************) + (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) @@ -14,7 +15,7 @@ Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub - spec_div spec_modulo spec_gcd spec_compare spec_eq_bool + spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd : nsimpl. Ltac nsimpl := autorewrite with nsimpl. @@ -219,6 +220,16 @@ Proof. intros. now zify. Qed. +(** Sqrt *) + +Program Instance sqrt_wd : Proper (eq==>eq) sqrt. + +Lemma sqrt_spec : forall n, 0<=n -> + (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)). +Proof. + intros n. zify. apply Zsqrt_spec. +Qed. + (** Even / Odd *) Definition Even n := exists m, n == 2*m. diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget index a54e85872d..7867b8caa0 100644 --- a/theories/Numbers/vo.itarget +++ b/theories/Numbers/vo.itarget @@ -48,6 +48,7 @@ NatInt/NZProperties.vo NatInt/NZDomain.vo NatInt/NZDiv.vo NatInt/NZPow.vo +NatInt/NZSqrt.vo Natural/Abstract/NAddOrder.vo Natural/Abstract/NAdd.vo Natural/Abstract/NAxioms.vo @@ -63,6 +64,7 @@ Natural/Abstract/NDiv.vo Natural/Abstract/NMaxMin.vo Natural/Abstract/NParity.vo Natural/Abstract/NPow.vo +Natural/Abstract/NSqrt.vo Natural/BigN/BigN.vo Natural/BigN/Nbasic.vo Natural/BigN/NMake_gen.vo |