diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 13 |
2 files changed, 13 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 7cf3e7046..703897eba 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 e1dc5349b..f072fc24a 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. |