Making the sumbool functions transparent, so that they can used to

compute even inside Coq.


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

1 files changed, 19 insertions, 13 deletions

diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index f5d6fda5b..7fbc56ee8 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -37,7 +37,7 @@ Section decidability.
 
 Variables x,y : Z.
 
-Theorem Z_eq_dec : {x=y}+{~x=y}.
+Definition Z_eq_dec : {x=y}+{~x=y}.
 Proof.
 Apply Zcompare_rec with x:=x y:=y.
 Intro. Left. Elim (Zcompare_EGAL x y); Auto with arith.
@@ -47,7 +47,7 @@ Intro H3. Right. Elim (Zcompare_EGAL x y). Intros H1 H2. Unfold not. Intro H4.
   Rewrite (H2 H4) in H3. Discriminate H3.
 Defined. 
 
-Theorem Z_lt_dec : {(Zlt x y)}+{~(Zlt x y)}.
+Definition Z_lt_dec : {(Zlt x y)}+{~(Zlt x y)}.
 Proof.
 Unfold Zlt.
 Apply Zcompare_rec with x:=x y:=y; Intro H.
@@ -56,7 +56,7 @@ Left; Assumption.
 Right. Rewrite H. Discriminate.
 Defined.
 
-Theorem Z_le_dec : {(Zle x y)}+{~(Zle x y)}.
+Definition Z_le_dec : {(Zle x y)}+{~(Zle x y)}.
 Proof.
 Unfold Zle.
 Apply Zcompare_rec with x:=x y:=y; Intro H.
@@ -65,7 +65,7 @@ Left. Rewrite H. Discriminate.
 Right. Tauto.
 Defined.
 
-Theorem Z_gt_dec : {(Zgt x y)}+{~(Zgt x y)}.
+Definition Z_gt_dec : {(Zgt x y)}+{~(Zgt x y)}.
 Proof.
 Unfold Zgt.
 Apply Zcompare_rec with x:=x y:=y; Intro H.
@@ -74,7 +74,7 @@ Right. Rewrite H. Discriminate.
 Left; Assumption.
 Defined.
 
-Theorem Z_ge_dec : {(Zge x y)}+{~(Zge x y)}.
+Definition Z_ge_dec : {(Zge x y)}+{~(Zge x y)}.
 Proof.
 Unfold Zge.
 Apply Zcompare_rec with x:=x y:=y; Intro H.
@@ -83,26 +83,30 @@ Right. Tauto.
 Left. Rewrite H. Discriminate.
 Defined.
 
-Theorem Z_lt_ge_dec : {`x < y`}+{`x >= y`}.
-Proof Z_lt_dec.
+Definition Z_lt_ge_dec : {`x < y`}+{`x >= y`}.
+Proof.
+Exact Z_lt_dec.
+Defined.
 
-Theorem Z_le_gt_dec : {`x <= y`}+{`x > y`}.
+Definition Z_le_gt_dec : {`x <= y`}+{`x > y`}.
 Proof.
 Elim Z_le_dec; Auto with arith.
 Intro. Right. Apply not_Zle; Auto with arith.
 Defined.
 
-Theorem Z_gt_le_dec : {`x > y`}+{`x <= y`}.
-Proof Z_gt_dec.
+Definition Z_gt_le_dec : {`x > y`}+{`x <= y`}.
+Proof.
+Exact Z_gt_dec.
+Defined.
 
-Theorem Z_ge_lt_dec : {`x >= y`}+{`x < y`}.
+Definition Z_ge_lt_dec : {`x >= y`}+{`x < y`}.
 Proof.
 Elim Z_ge_dec; Auto with arith.
 Intro. Right. Apply not_Zge; Auto with arith.
 Defined.
 
 
-Theorem Z_le_lt_eq_dec : `x <= y` -> {`x < y`}+{x=y}.
+Definition Z_le_lt_eq_dec : `x <= y` -> {`x < y`}+{x=y}.
 Proof.
 Intro H.
 Apply Zcompare_rec with x:=x y:=y.
@@ -116,7 +120,9 @@ End decidability.
 
 
 Definition Z_zerop : (x:Z){(`x = 0`)}+{(`x <> 0`)}.
-Proof [x:Z](Z_eq_dec x ZERO).
+Proof.
+Exact [x:Z](Z_eq_dec x ZERO).
+Defined.
 
 Definition Z_notzerop := [x:Z](sumbool_not ? ? (Z_zerop x)).