From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/ZArith/Zsqrt_compat.v | 233 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 233 insertions(+)
 create mode 100644 theories/ZArith/Zsqrt_compat.v

(limited to 'theories/ZArith/Zsqrt_compat.v')

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
-- 
cgit v1.2.3