From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- theories/ZArith/Zsqrt.v | 215 ------------------------------------------------ 1 file changed, 215 deletions(-) delete mode 100644 theories/ZArith/Zsqrt.v (limited to 'theories/ZArith/Zsqrt.v') diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v deleted file mode 100644 index 1a67bbb2..00000000 --- a/theories/ZArith/Zsqrt.v +++ /dev/null @@ -1,215 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - match constr:X1 with - | context [1%positive] => fail 1 - | _ => rewrite (BinInt.Zpos_xI X1) - end - | |- context [(Zpos (xO ?X1))] => - match constr:X1 with - | 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. - -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) - (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) - (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) - (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) - (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); try omega. -Defined. - -(** Define with integer input, but with a strong (readable) specification. *) -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 - 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 - (fun s:Z => - {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 - {s : Z & - {r : Z | - Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}} - (h (refl_equal Datatypes.Gt)) - | Z0 => - fun h => - existS - (fun s:Z => - {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_simplify (s*s) ((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 => - match Zsqrt (Zpos p) (Zorder.Zle_0_pos p) with - | existS s _ => s - end - | 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). -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. - -(** Positivity *) - -Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n. -Proof. - intros n m; case (Zsqrt_interval n); auto with zarith. - intros H1 H2; case (Zle_or_lt 0 (Zsqrt_plain n)); auto. - intros H3; contradict H2; auto; apply Zle_not_lt. - apply Zle_trans with ( 2 := H1 ). - replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1)) - with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1)); - auto with zarith. - ring. -Qed. - -(** Direct correctness on squares. *) - -Theorem Zsqrt_square_id: forall a, 0 <= a -> Zsqrt_plain (a * a) = a. -Proof. - intros a H. - generalize (Zsqrt_plain_is_pos (a * a)); auto with zarith; intros Haa. - case (Zsqrt_interval (a * a)); auto with zarith. - intros H1 H2. - case (Zle_or_lt a (Zsqrt_plain (a * a))); intros H3; auto. - case Zle_lt_or_eq with (1:=H3); auto; clear H3; intros H3. - contradict H1; auto; apply Zlt_not_le; auto with zarith. - apply Zle_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith. - apply Zmult_lt_compat_r; auto with zarith. - contradict H2; auto; apply Zle_not_lt; auto with zarith. - apply Zmult_le_compat; auto with zarith. -Qed. - -(** [Zsqrt_plain] is increasing *) - -Theorem Zsqrt_le: - forall p q, 0 <= p <= q -> Zsqrt_plain p <= Zsqrt_plain q. -Proof. - intros p q [H1 H2]; case Zle_lt_or_eq with (1:=H2); clear H2; intros H2; - [ | subst q; auto with zarith]. - case (Zle_or_lt (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3. - assert (Hp: (0 <= Zsqrt_plain q)). - apply Zsqrt_plain_is_pos; auto with zarith. - absurd (q <= p); auto with zarith. - apply Zle_trans with ((Zsqrt_plain q + 1) * (Zsqrt_plain q + 1)). - case (Zsqrt_interval q); auto with zarith. - apply Zle_trans with (Zsqrt_plain p * Zsqrt_plain p); auto with zarith. - apply Zmult_le_compat; auto with zarith. - case (Zsqrt_interval p); auto with zarith. -Qed. - - -- cgit v1.2.3