diff options
Diffstat (limited to 'flocq/Calc/Fcalc_sqrt.v')
-rw-r--r-- | flocq/Calc/Fcalc_sqrt.v | 108 |
1 files changed, 3 insertions, 105 deletions
diff --git a/flocq/Calc/Fcalc_sqrt.v b/flocq/Calc/Fcalc_sqrt.v index 2ed32347..5f541d83 100644 --- a/flocq/Calc/Fcalc_sqrt.v +++ b/flocq/Calc/Fcalc_sqrt.v @@ -28,108 +28,6 @@ Require Import Fcalc_digits. Section Fcalc_sqrt. -Fixpoint Zsqrt_aux (p : positive) : Z * Z := - match p with - | xH => (1, 0)%Z - | xO xH => (1, 1)%Z - | xI xH => (1, 2)%Z - | xO (xO p) => - let (q, r) := Zsqrt_aux p in - let r' := (4 * r)%Z in - let d := (r' - (4 * q + 1))%Z in - if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z - | xO (xI p) => - let (q, r) := Zsqrt_aux p in - let r' := (4 * r + 2)%Z in - let d := (r' - (4 * q + 1))%Z in - if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z - | xI (xO p) => - let (q, r) := Zsqrt_aux p in - let r' := (4 * r + 1)%Z in - let d := (r' - (4 * q + 1))%Z in - if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z - | xI (xI p) => - let (q, r) := Zsqrt_aux p in - let r' := (4 * r + 3)%Z in - let d := (r' - (4 * q + 1))%Z in - if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z - end. - -Lemma Zsqrt_ind : - forall P : positive -> Prop, - P xH -> P (xO xH) -> P (xI xH) -> - ( forall p, P p -> P (xO (xO p)) /\ P (xO (xI p)) /\ P (xI (xO p)) /\ P (xI (xI p)) ) -> - forall p, P p. -Proof. -intros P H1 H2 H3 Hp. -fix 1. -intros [[p|p|]|[p|p|]|]. -refine (proj2 (proj2 (proj2 (Hp p _)))). -apply Zsqrt_ind. -refine (proj1 (proj2 (proj2 (Hp p _)))). -apply Zsqrt_ind. -exact H3. -refine (proj1 (proj2 (Hp p _))). -apply Zsqrt_ind. -refine (proj1 (Hp p _)). -apply Zsqrt_ind. -exact H2. -exact H1. -Qed. - -Lemma Zsqrt_aux_correct : - forall p, - let (q, r) := Zsqrt_aux p in - Zpos p = (q * q + r)%Z /\ (0 <= r <= 2 * q)%Z. -Proof. -intros p. -elim p using Zsqrt_ind ; clear p. -now repeat split. -now repeat split. -now repeat split. -intros p. -Opaque Zmult. simpl. Transparent Zmult. -destruct (Zsqrt_aux p) as (q, r). -intros (Hq, Hr). -change (Zpos p~0~0) with (4 * Zpos p)%Z. -change (Zpos p~0~1) with (4 * Zpos p + 1)%Z. -change (Zpos p~1~0) with (4 * Zpos p + 2)%Z. -change (Zpos p~1~1) with (4 * Zpos p + 3)%Z. -rewrite Hq. clear Hq. -repeat split. -generalize (Zlt_cases (4 * r - (4 * q + 1)) 0). -case Zlt_bool ; ( split ; [ ring | omega ] ). -generalize (Zlt_cases (4 * r + 2 - (4 * q + 1)) 0). -case Zlt_bool ; ( split ; [ ring | omega ] ). -generalize (Zlt_cases (4 * r + 1 - (4 * q + 1)) 0). -case Zlt_bool ; ( split ; [ ring | omega ] ). -generalize (Zlt_cases (4 * r + 3 - (4 * q + 1)) 0). -case Zlt_bool ; ( split ; [ ring | omega ] ). -Qed. - -(** Computes the integer square root and its remainder, but - without carrying a proof, contrarily to the operation of - the standard libary. *) - -Definition Zsqrt p := - match p with - | Zpos p => Zsqrt_aux p - | _ => (0, 0)%Z - end. - -Theorem Zsqrt_correct : - forall x, - (0 <= x)%Z -> - let (q, r) := Zsqrt x in - x = (q * q + r)%Z /\ (0 <= r <= 2 * q)%Z. -Proof. -unfold Zsqrt. -intros [|p|p] Hx. -now repeat split. -apply Zsqrt_aux_correct. -now elim Hx. -Qed. - Variable beta : radix. Notation bpow e := (bpow beta e). @@ -160,7 +58,7 @@ Definition Fsqrt_core prec m e := | Zpos p => (m * Zpower_pos beta p)%Z | _ => m end in - let (q, r) := Zsqrt m' in + let (q, r) := Z.sqrtrem m' in let l := if Zeq_bool r 0 then loc_Exact else loc_Inexact (if Zle_bool r q then Lt else Gt) in @@ -236,8 +134,8 @@ now apply Zpower_gt_0. now elim He2. clearbody m'. destruct Hs as (Hs1, (Hs2, Hs3)). -generalize (Zsqrt_correct m' (Zlt_le_weak _ _ Hs3)). -destruct (Zsqrt m') as (q, r). +generalize (Z.sqrtrem_spec m' (Zlt_le_weak _ _ Hs3)). +destruct (Z.sqrtrem m') as (q, r). intros (Hq, Hr). rewrite <- Hs1. clear Hs1. split. |