diff options
author | 2006-10-17 12:53:34 +0000 | |
---|---|---|
committer | 2006-10-17 12:53:34 +0000 | |
commit | 28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch) | |
tree | 63cdf18cd47260eb90550f62f7b22e2e2e208f6c /theories/ZArith/Zsqrt.v | |
parent | 744e7f6a319f4d459a3cc2309f575d43041d75aa (diff) |
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zsqrt.v')
-rw-r--r-- | theories/ZArith/Zsqrt.v | 177 |
1 files changed, 89 insertions, 88 deletions
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 804ab679d..79fce8964 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -20,66 +20,66 @@ 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) _ _ @@ -94,40 +94,40 @@ 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 _) @@ -139,25 +139,26 @@ Defined. 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. |