summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zsqrt_compat.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
commit39efc41237ec906226a3a53d7396d51173495204 (patch)
tree87cd58d72d43469d2a2a0a127c1060d7c9e0206b /theories/ZArith/Zsqrt_compat.v
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'theories/ZArith/Zsqrt_compat.v')
-rw-r--r--theories/ZArith/Zsqrt_compat.v233
1 files changed, 233 insertions, 0 deletions
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
new file mode 100644
index 00000000..4584c3f8
--- /dev/null
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -0,0 +1,233 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import ZArithRing.
+Require Import Omega.
+Require Export ZArith_base.
+Open Local Scope Z_scope.
+
+(** THIS FILE IS DEPRECATED
+
+ Instead of the various [Zsqrt] defined here, please use rather
+ [Z.sqrt] (or [Z.sqrtrem]). The latter are pure functions without
+ proof parts, and more results are available about them.
+ Some equivalence proofs between the old and the new versions
+ can be found below. Importing ZArith will provides by default
+ the new versions.
+
+*)
+
+(**********************************************************************)
+(** Definition and properties of square root on Z *)
+
+(** The following tactic replaces all instances of (POS (xI ...)) by
+ `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))] =>
+ 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.
+
+
+(** Equivalence between Zsqrt_plain and [Z.sqrt] *)
+
+Lemma Zsqrt_equiv : forall n, Zsqrt_plain n = Z.sqrt n.
+Proof.
+ intros. destruct (Z_le_gt_dec 0 n).
+ symmetry. apply Z.sqrt_unique; trivial.
+ now apply Zsqrt_interval.
+ now destruct n.
+Qed. \ No newline at end of file