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

1 files changed, 11 insertions, 11 deletions

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)).