diff options
Diffstat (limited to 'theories/ZArith/Zsqrt.v')
-rw-r--r-- | theories/ZArith/Zsqrt.v | 185 |
1 files changed, 93 insertions, 92 deletions
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index cf4acb5f..9893bed3 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zsqrt.v 6199 2004-10-11 11:39:18Z herbelin $ *) +(* $Id: Zsqrt.v 9245 2006-10-17 12:53:34Z notin $ *) +Require Import ZArithRing. Require Import Omega. Require Export ZArith_base. -Require Export ZArithRing. Open Local Scope Z_scope. (**********************************************************************) @@ -20,73 +20,73 @@ Open Local Scope Z_scope. `2*(POS ...)+1`, but only when ... is not made only with xO, XI, or xH. *) Ltac compute_POS := match goal with - | |- context [(Zpos (xI ?X1))] => + | |- context [(Zpos (xI ?X1))] => match constr:X1 with - | context [1%positive] => fail 1 - | _ => rewrite (BinInt.Zpos_xI X1) + | context [1%positive] => fail 1 + | _ => rewrite (BinInt.Zpos_xI X1) end - | |- context [(Zpos (xO ?X1))] => + | |- context [(Zpos (xO ?X1))] => match constr:X1 with - | context [1%positive] => fail 1 - | _ => rewrite (BinInt.Zpos_xO X1) + | context [1%positive] => fail 1 + | _ => rewrite (BinInt.Zpos_xO X1) end end. Inductive sqrt_data (n:Z) : Set := - c_sqrt : forall s r:Z, n = s * s + r -> 0 <= r <= 2 * s -> sqrt_data n. + c_sqrt : forall s r:Z, n = s * s + r -> 0 <= r <= 2 * s -> sqrt_data n. Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). -refine - (fix sqrtrempos (p:positive) : sqrt_data (Zpos p) := - match p return sqrt_data (Zpos p) with - | xH => c_sqrt 1 1 0 _ _ - | xO xH => c_sqrt 2 1 1 _ _ - | xI xH => c_sqrt 3 1 2 _ _ - | xO (xO p') => - match sqrtrempos p' with - | c_sqrt s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r') with - | left Hle => - c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1) + refine + (fix sqrtrempos (p:positive) : sqrt_data (Zpos p) := + match p return sqrt_data (Zpos p) with + | xH => c_sqrt 1 1 0 _ _ + | xO xH => c_sqrt 2 1 1 _ _ + | xI xH => c_sqrt 3 1 2 _ _ + | xO (xO p') => + match sqrtrempos p' with + | c_sqrt s' r' Heq Hint => + match Z_le_gt_dec (4 * s' + 1) (4 * r') with + | left Hle => + c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1) (4 * r' - (4 * s' + 1)) _ _ - | right Hgt => c_sqrt (Zpos (xO (xO p'))) (2 * s') (4 * r') _ _ - end - end - | xO (xI p') => - match sqrtrempos p' with - | c_sqrt s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with - | left Hle => - c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1) + | right Hgt => c_sqrt (Zpos (xO (xO p'))) (2 * s') (4 * r') _ _ + end + end + | xO (xI p') => + match sqrtrempos p' with + | c_sqrt s' r' Heq Hint => + match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with + | left Hle => + c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1) (4 * r' + 2 - (4 * s' + 1)) _ _ - | right Hgt => - c_sqrt (Zpos (xO (xI p'))) (2 * s') (4 * r' + 2) _ _ - end - end - | xI (xO p') => - match sqrtrempos p' with - | c_sqrt s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with - | left Hle => - c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1) + | right Hgt => + c_sqrt (Zpos (xO (xI p'))) (2 * s') (4 * r' + 2) _ _ + end + end + | xI (xO p') => + match sqrtrempos p' with + | c_sqrt s' r' Heq Hint => + match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with + | left Hle => + c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1) (4 * r' + 1 - (4 * s' + 1)) _ _ - | right Hgt => - c_sqrt (Zpos (xI (xO p'))) (2 * s') (4 * r' + 1) _ _ - end - end - | xI (xI p') => - match sqrtrempos p' with - | c_sqrt s' r' Heq Hint => - match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with - | left Hle => - c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1) + | right Hgt => + c_sqrt (Zpos (xI (xO p'))) (2 * s') (4 * r' + 1) _ _ + end + end + | xI (xI p') => + match sqrtrempos p' with + | c_sqrt s' r' Heq Hint => + match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with + | left Hle => + c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1) (4 * r' + 3 - (4 * s' + 1)) _ _ | right Hgt => c_sqrt (Zpos (xI (xI p'))) (2 * s') (4 * r' + 3) _ _ end end end); clear sqrtrempos; repeat compute_POS; - try (try rewrite Heq; ring; fail); try omega. + try (try rewrite Heq; ring); try omega. Defined. (** Define with integer input, but with a strong (readable) specification. *) @@ -94,70 +94,71 @@ Definition Zsqrt : forall x:Z, 0 <= x -> {s : Z & {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}}. -refine - (fun x => - match - x - return + refine + (fun x => + match + x + return 0 <= x -> {s : Z & {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}} - with - | Zpos p => - fun h => - match sqrtrempos p with - | c_sqrt s r Heq Hint => - existS + with + | Zpos p => + fun h => + match sqrtrempos p with + | c_sqrt s r Heq Hint => + existS (fun s:Z => - {r : Z | - Zpos p = s * s + r /\ s * s <= Zpos p < (s + 1) * (s + 1)}) + {r : Z | + Zpos p = s * s + r /\ s * s <= Zpos p < (s + 1) * (s + 1)}) s (exist - (fun r:Z => - Zpos p = s * s + r /\ - s * s <= Zpos p < (s + 1) * (s + 1)) r _) - end - | Zneg p => - fun h => - False_rec + (fun r:Z => + Zpos p = s * s + r /\ + s * s <= Zpos p < (s + 1) * (s + 1)) r _) + end + | Zneg p => + fun h => + False_rec {s : Z & - {r : Z | - Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}} + {r : Z | + Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}} (h (refl_equal Datatypes.Gt)) - | Z0 => - fun h => - existS + | Z0 => + fun h => + existS (fun s:Z => - {r : Z | 0 = s * s + r /\ s * s <= 0 < (s + 1) * (s + 1)}) 0 + {r : Z | 0 = s * s + r /\ s * s <= 0 < (s + 1) * (s + 1)}) 0 (exist (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0 _) end); try omega. -split; [ omega | rewrite Heq; ring ((s + 1) * (s + 1)); omega ]. +split; [ omega | rewrite Heq; ring_simplify ((s + 1) * (s + 1)); omega ]. Defined. (** Define a function of type Z->Z that computes the integer square root, but only for positive numbers, and 0 for others. *) Definition Zsqrt_plain (x:Z) : Z := match x with - | Zpos p => + | Zpos p => match Zsqrt (Zpos p) (Zorder.Zle_0_pos p) with - | existS s _ => s + | existS s _ => s end - | Zneg p => 0 - | Z0 => 0 + | Zneg p => 0 + | Z0 => 0 end. (** A basic theorem about Zsqrt_plain *) Theorem Zsqrt_interval : - forall n:Z, - 0 <= n -> - Zsqrt_plain n * Zsqrt_plain n <= n < - (Zsqrt_plain n + 1) * (Zsqrt_plain n + 1). -intros x; case x. -unfold Zsqrt_plain in |- *; omega. -intros p; unfold Zsqrt_plain in |- *; - case (Zsqrt (Zpos p) (Zorder.Zle_0_pos p)). -intros s [r [Heq Hint]] Hle; assumption. -intros p Hle; elim Hle; auto. + forall n:Z, + 0 <= n -> + Zsqrt_plain n * Zsqrt_plain n <= n < + (Zsqrt_plain n + 1) * (Zsqrt_plain n + 1). +Proof. + intros x; case x. + unfold Zsqrt_plain in |- *; omega. + intros p; unfold Zsqrt_plain in |- *; + case (Zsqrt (Zpos p) (Zorder.Zle_0_pos p)). + intros s [r [Heq Hint]] Hle; assumption. + intros p Hle; elim Hle; auto. Qed. |