Adding file theories/ZArith/Zsqrt.v that contains a square root function.

actually three functions are provided, one working on positive numbers (it
is structurally recursive), one with a strong specification (Zsqrt), and one with
a weak specification (Zsqrt_plain).  For the function with a weak specification
an extra theorem is also provided.

The decision functions in ZArith_dec have been made transparent so that computation
with the square root function also becomes possible with Lazy Beta Iota Delta Zeta.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2770 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 147 insertions, 12 deletions

diff --git a/.depend.coq b/.depend.coq
index 49693cd25..f057e2793 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -111,6 +111,7 @@ theories/Lists/Streams.vo: theories/Lists/Streams.v
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith.vo
 theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/ring/ZArithRing.vo theories/ZArith/Zcomplements.vo
 theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
 theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo
diff --git a/Makefile b/Makefile
index b5ff0809b..4f6463060 100644
--- a/Makefile
+++ b/Makefile
@@ -454,7 +454,7 @@ ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/Zmisc.vo       theories/ZArith/zarith_aux.vo \
 	 theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
 	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
-	 theories/ZArith/Zdiv.vo
+	 theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo
 
 LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo \
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index de9fb0aed..f5d6fda5b 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -18,7 +18,7 @@ Require Zsyntax.
 Lemma Dcompare_inf : (r:relation) {r=EGAL} + {r=INFERIEUR} + {r=SUPERIEUR}.
 Proof.
 Induction r; Auto with arith. 
-Qed.
+Defined.
 
 Lemma Zcompare_rec :
   (P:Set)(x,y:Z)
@@ -30,7 +30,7 @@ Proof.
 Intros P x y H1 H2 H3.
 Elim (Dcompare_inf (Zcompare x y)).
 Intro H. Elim H; Auto with arith. Auto with arith.
-Qed.
+Defined.
 
 
 Section decidability.
@@ -45,7 +45,7 @@ Intro H3. Right. Elim (Zcompare_EGAL x y). Intros H1 H2. Unfold not. Intro H4.
   Rewrite (H2 H4) in H3. Discriminate H3.
 Intro H3. Right. Elim (Zcompare_EGAL x y). Intros H1 H2. Unfold not. Intro H4.
   Rewrite (H2 H4) in H3. Discriminate H3.
-Qed. 
+Defined. 
 
 Theorem Z_lt_dec : {(Zlt x y)}+{~(Zlt x y)}.
 Proof.
@@ -54,7 +54,7 @@ Apply Zcompare_rec with x:=x y:=y; Intro H.
 Right. Rewrite H. Discriminate.
 Left; Assumption.
 Right. Rewrite H. Discriminate.
-Qed.
+Defined.
 
 Theorem Z_le_dec : {(Zle x y)}+{~(Zle x y)}.
 Proof.
@@ -63,7 +63,7 @@ Apply Zcompare_rec with x:=x y:=y; Intro H.
 Left. Rewrite H. Discriminate.
 Left. Rewrite H. Discriminate.
 Right. Tauto.
-Qed.
+Defined.
 
 Theorem Z_gt_dec : {(Zgt x y)}+{~(Zgt x y)}.
 Proof.
@@ -72,7 +72,7 @@ Apply Zcompare_rec with x:=x y:=y; Intro H.
 Right. Rewrite H. Discriminate.
 Right. Rewrite H. Discriminate.
 Left; Assumption.
-Qed.
+Defined.
 
 Theorem Z_ge_dec : {(Zge x y)}+{~(Zge x y)}.
 Proof.
@@ -81,7 +81,7 @@ Apply Zcompare_rec with x:=x y:=y; Intro H.
 Left. Rewrite H. Discriminate.
 Right. Tauto.
 Left. Rewrite H. Discriminate.
-Qed.
+Defined.
 
 Theorem Z_lt_ge_dec : {`x < y`}+{`x >= y`}.
 Proof Z_lt_dec.
@@ -90,7 +90,7 @@ Theorem Z_le_gt_dec : {`x <= y`}+{`x > y`}.
 Proof.
 Elim Z_le_dec; Auto with arith.
 Intro. Right. Apply not_Zle; Auto with arith.
-Qed.
+Defined.
 
 Theorem Z_gt_le_dec : {`x > y`}+{`x <= y`}.
 Proof Z_gt_dec.
@@ -99,7 +99,7 @@ Theorem Z_ge_lt_dec : {`x >= y`}+{`x < y`}.
 Proof.
 Elim Z_ge_dec; Auto with arith.
 Intro. Right. Apply not_Zge; Auto with arith.
-Qed.
+Defined.
 
 
 Theorem Z_le_lt_eq_dec : `x <= y` -> {`x < y`}+{x=y}.
@@ -109,13 +109,13 @@ Apply Zcompare_rec with x:=x y:=y.
 Intro. Right. Elim (Zcompare_EGAL x y); Auto with arith.
 Intro. Left. Elim (Zcompare_EGAL x y); Auto with arith.
 Intro H1. Absurd `x > y`; Auto with arith.
-Qed.
+Defined.
 
 
 End decidability.
 
 
-Theorem Z_zerop : (x:Z){(`x = 0`)}+{(`x <> 0`)}.
+Definition Z_zerop : (x:Z){(`x = 0`)}+{(`x <> 0`)}.
 Proof [x:Z](Z_eq_dec x ZERO).
 
 Definition Z_notzerop := [x:Z](sumbool_not ? ? (Z_zerop x)).
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
new file mode 100644
index 000000000..9939f838f
--- /dev/null
+++ b/theories/ZArith/Zsqrt.v
@@ -0,0 +1,134 @@
+Require Export ZArith.
+Require Export ZArithRing.
+Require Export Omega.
+
+(* 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.
+   
+   It is very important to put (Fail 1) and not (Fail 2) in this
+   tactic.  This is not very well documented anywhere, but it seems, that
+   Fail 2 makes the "Match Context" tactic fail, while (Fail 1) only
+   makes the clause fail. *)
+Tactic Definition compute_POS :=
+ (Match Context With
+ | [|- ?] -> Fail
+ | [|- [(POS (xI ?1))]] -> Let v = ?1 In 
+                          (Match v With
+                            | [ [xH] ] ->
+                              (Fail 1)
+                            |_->
+                              Rewrite (POS_xI v))
+ | [ |- [(POS (xO ?1))]] -> Let v = ?1 In
+                           Match v With
+                            |[ [xH] ]->
+                              (Fail 1)
+                            |[?]->
+                              Rewrite (POS_xO v)).
+
+
+Inductive sqrt_data [n : Z] : Set :=
+  c_sqrt: (s, r :Z)`n=s*s+r`->`0<=r<=2*s`->(sqrt_data n) .
+
+Definition sqrtrempos: (p : positive)  (sqrt_data (POS p)).
+Refine (Fix sqrtrempos {
+         sqrtrempos [p : positive] : (sqrt_data (POS p)) :=
+            <[p : ?]  (sqrt_data (POS p))> Cases p of
+                xH => (c_sqrt `1` `1` `0` ? ?)
+               | (xO xH) => (c_sqrt `2` `1` `1` ? ?)
+               | (xI xH) => (c_sqrt `3` `1` `2` ? ?)
+               | (xO (xO p')) =>
+                   Cases (sqrtrempos p') of
+                     (c_sqrt s' r' Heq Hint) =>
+                       Cases (Z_le_gt_dec `4*s'+1` `4*r'`) of
+                         (left Hle) =>
+                           (c_sqrt (POS (xO (xO p'))) `2*s'+1` `4*r'-(4*s'+1)` ? ?)
+                        | (right Hgt) =>
+                            (c_sqrt (POS (xO (xO p'))) `2*s'` `4*r'` ? ?)
+                       end
+                   end
+               | (xO (xI p')) =>
+                   Cases (sqrtrempos p') of
+                     (c_sqrt s' r' Heq Hint) =>
+                       Cases
+                        (Z_le_gt_dec `4*s'+1` `4*r'+2`) of
+                         (left Hle) =>
+                           (c_sqrt 
+			     (POS (xO (xI p'))) `2*s'+1` `4*r'+2-(4*s'+1)` ? ?)
+                        | (right Hgt) =>
+                            (c_sqrt (POS (xO (xI p'))) `2*s'` `4*r'+2` ? ?)
+                       end
+                   end
+               | (xI (xO p')) =>
+                   Cases (sqrtrempos p') of
+                     (c_sqrt s' r' Heq Hint) =>
+                       Cases
+                        (Z_le_gt_dec `4*s'+1` `4*r'+1`) of
+                         (left Hle) =>
+                           (c_sqrt
+                            (POS (xI (xO p'))) `2*s'+1` `4*r'+1-(4*s'+1)` ? ?)
+                        | (right Hgt) =>
+                            (c_sqrt (POS (xI (xO p'))) `2*s'` `4*r'+1` ? ?)
+                       end
+                   end
+               | (xI (xI p')) =>
+                   Cases (sqrtrempos p') of
+                     (c_sqrt s' r' Heq Hint) =>
+                       Cases
+                        (Z_le_gt_dec `4*s'+1` `4*r'+3`) of
+                         (left Hle) =>
+                           (c_sqrt
+                            (POS (xI (xI p'))) `2*s'+1` `4*r'+3-(4*s'+1)` ? ?)
+                        | (right Hgt) =>
+                            (c_sqrt (POS (xI (xI p'))) `2*s'` `4*r'+3` ? ?)
+                       end
+                   end
+            end
+        }); Clear sqrtrempos; Repeat compute_POS;
+ Try (Try Rewrite Heq; Ring; Fail); Try Omega.
+Defined.
+
+(** Define with integer input, but with a strong (readable) specification. *)
+Definition Zsqrt : (x:Z)`0<=x`->{s:Z & {r:Z | x=`s*s+r` /\ `s*s<=x<(s+1)*(s+1)`}}.
+Refine [x]
+   <[x:Z]`0<=x`->{s:Z & {r:Z | x=`s*s+r` /\ `s*s<=x<(s+1)*(s+1)`}}>Cases x of
+       (POS p) => [h]Cases (sqrtrempos p) of
+                    (c_sqrt s r Heq Hint) =>
+                  (existS ? [s:Z]{r:Z | `(POS p)=s*s+r` /\ 
+		                         `s*s<=(POS p)<(s+1)*(s+1)`}
+		   s
+                    (exist Z [r:Z]((POS p)=`s*s+r` /\ `s*s<=(POS p)<(s+1)*(s+1)`)
+                       r ?))
+                  end
+     | (NEG p) => [h](False_rec 
+		         {s:Z & {r:Z |
+			     (NEG p)=`s*s+r` /\ `s*s<=(NEG p)<(s+1)*(s+1)`}}
+                         (h (refl_equal ? SUPERIEUR)))
+     | ZERO => [h](existS ? [s:Z]{r:Z | `0=s*s+r` /\ `s*s<=0<(s+1)*(s+1)`}
+		     `0` (exist Z [r:Z](`0=0*0+r`/\`0*0<=0<(0+1)*(0+1)`)
+		     `0` ?))
+     end;Try Omega.
+Split;[Omega|Rewrite Heq;Ring `(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 : Z->Z :=
+  [x]Cases x of
+    (POS p)=>Cases (Zsqrt (POS p) (ZERO_le_POS p)) of (existS s _) => s end
+   |(NEG p)=>`0`
+   |ZERO=>`0`
+   end.
+
+(** A basic theorem about Zsqrt_plain *)
+Theorem Zsqrt_interval :(x:Z)`0<=x`->
+  `(Zsqrt_plain x)*(Zsqrt_plain x)<= x < ((Zsqrt_plain x)+1)*((Zsqrt_plain x)+1)`.
+Intros x;Case x.
+Unfold Zsqrt_plain;Omega.
+Intros p;Unfold Zsqrt_plain;Case (Zsqrt (POS p) (ZERO_le_POS p)).
+Intros s (r,(Heq,Hint)) Hle;Assumption.
+Intros p Hle;Elim Hle;Auto.
+Qed.
+
+