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

7 files changed, 65 insertions, 55 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index d729253b3..67218de83 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -13,17 +13,17 @@ Require Lt.
 Require Gt.
 Require Decidable.
 
-Theorem zerop : (n:nat){n=O}+{lt O n}.
+Definition zerop : (n:nat){n=O}+{lt O n}.
 NewDestruct n; Auto with arith.
-Qed.
+Defined.
 
-Theorem lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
+Definition lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
 Proof.
 NewInduction n; NewInduction m; Auto with arith.
 Elim (IHn m).
 NewInduction 1; Auto with arith.
 Auto with arith.
-Qed.
+Defined.
 
 Lemma gt_eq_gt_dec : (n,m:nat)({(gt m n)}+{n=m})+{(gt n m)}.
 Proof lt_eq_lt_dec.
@@ -35,25 +35,28 @@ Auto with arith.
 NewInduction m.
 Auto with arith.
 Elim (IHn m); Auto with arith.
-Qed.
+Defined.
 
-Lemma le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}.
-Proof le_lt_dec.
+Definition le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}.
+Proof.
+Exact le_lt_dec.
+Defined.
 
-Lemma le_ge_dec : (n,m:nat) {le n m} + {ge n m}.
+Definition le_ge_dec : (n,m:nat) {le n m} + {ge n m}.
 Proof.
 Intros; Elim (le_lt_dec n m); Auto with arith.
-Qed.
-
-Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
-Proof le_lt_dec.
+Defined.
 
+Definition le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
+Proof.
+Exact le_lt_dec.
+Defined.
 
-Theorem le_lt_eq_dec : (n,m:nat)(le n m)->({(lt n m)}+{n=m}).
+Definition le_lt_eq_dec : (n,m:nat)(le n m)->({(lt n m)}+{n=m}).
 Proof.
 Intros; Elim (lt_eq_lt_dec n m); Auto with arith.
 Intros; Absurd (lt m n); Auto with arith.
-Qed.
+Defined.
 
 (** Proofs of decidability *)
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 0cd20e094..5263cb375 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -140,14 +140,14 @@ Proof.
   Intros. Discriminate H.
 Qed.
 
-Lemma plus_is_one : 
+Definition plus_is_one : 
       (m,n:nat) (m+n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
 Proof.
   NewDestruct m; Auto.
   NewDestruct n; Auto.
   Intros. 
   Simpl in H. Discriminate H.
-Qed.
+Defined.
 
 Lemma plus_permute_2_in_4 : (a,b,c,d:nat) ((a+b)+(c+d))=((a+c)+(b+d)).
 Proof.
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 9cb4c1bb2..f2c9bfc8e 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -260,9 +260,10 @@ Lemma orb_true_b : (b:bool)(orb true b)=true.
 Trivial with bool.
 Qed.
 
-Lemma orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}.
+Definition orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}.
 NewDestruct b1; Simpl; Auto with bool.
-Qed.
+Defined.
+
 Lemma orb_false_intro 
     : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false.
 Intros b1 b2 H1 H2; Rewrite H1; Rewrite H2; Trivial with bool.
@@ -374,10 +375,10 @@ Lemma andb_true_b : (b:bool)(andb true b)=b.
 Trivial with bool.
 Qed.
 
-Lemma andb_false_elim : 
+Definition andb_false_elim : 
     (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}.
 NewDestruct b1; Simpl; Auto with bool.
-Qed.
+Defined.
 Hints Resolve andb_false_elim : bool v62.
 
 Lemma andb_neg_b :
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 84e74f86b..6f3adcf32 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -15,22 +15,22 @@
 
 (** A boolean is either [true] or [false], and this is decidable *)
 
-Lemma sumbool_of_bool : (b:bool) {b=true}+{b=false}.
+Definition sumbool_of_bool : (b:bool) {b=true}+{b=false}.
 Proof.
   Induction b; Auto.
-Qed.
+Defined.
 
 Hints Resolve sumbool_of_bool : bool.
 
-Lemma bool_eq_rec : (b:bool)(P:bool->Set)
+Definition bool_eq_rec : (b:bool)(P:bool->Set)
                     ((b=true)->(P true))->((b=false)->(P false))->(P b).
 Induction b; Auto.
-Qed.
+Defined.
 
-Lemma bool_eq_ind : (b:bool)(P:bool->Prop)
+Definition bool_eq_ind : (b:bool)(P:bool->Prop)
                     ((b=true)->(P true))->((b=false)->(P false))->(P b).
 Induction b; Auto.
-Qed.
+Defined.
 
 
 (*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
@@ -44,20 +44,20 @@ Variables A,B,C,D : Prop.
 Hypothesis H1 : {A}+{B}.
 Hypothesis H2 : {C}+{D}.
 
-Lemma sumbool_and : {A/\C}+{B\/D}.
+Definition sumbool_and : {A/\C}+{B\/D}.
 Proof.
 Case H1; Case H2; Auto.
-Qed.
+Defined.
 
-Lemma sumbool_or : {A\/C}+{B/\D}.
+Definition sumbool_or : {A\/C}+{B/\D}.
 Proof.
 Case H1; Case H2; Auto.
-Qed.
+Defined.
 
-Lemma sumbool_not : {B}+{A}.
+Definition sumbool_not : {B}+{A}.
 Proof.
 Case H1; Auto.
-Qed.
+Defined.
 
 End connectives.
 
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)).
 
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 5f1eb0721..ad5db4b53 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -242,7 +242,7 @@ Definition Zodd_bool :=
 		| _ => true
                end.
 
-Lemma Zeven_odd_dec : (z:Z) { (Zeven z) }+{ (Zodd z) }.
+Definition Zeven_odd_dec : (z:Z) { (Zeven z) }+{ (Zodd z) }.
 Proof.
   Intro z. Case z;
   [ Left; Compute; Trivial
@@ -254,9 +254,9 @@ Proof.
   Realizer Zeven_bool.
   Repeat Program; Compute; Trivial.
   i*)
-Qed.
+Defined.
 
-Lemma Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }.
+Definition Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }.
 Proof.
   Intro z. Case z;
   [ Left; Compute; Trivial
@@ -268,9 +268,9 @@ Proof.
   Realizer Zeven_bool.
   Repeat Program; Compute; Trivial.
   i*)
-Qed.
+Defined.
 
-Lemma Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }.
+Definition Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }.
 Proof.
   Intro z. Case z;
   [ Right; Compute; Trivial
@@ -282,7 +282,7 @@ Proof.
   Realizer Zodd_bool.
   Repeat Program; Compute; Trivial.
   i*)
-Qed.
+Defined.
 
 Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z).
 Proof.
@@ -486,14 +486,14 @@ Proof.
   Apply Zle_bool_imp_le. Assumption.
 Qed.
 
-Lemma Zle_bool_total : (x,y:Z) {(Zle_bool x y)=true}+{(Zle_bool y x)=true}.
+Definition Zle_bool_total : (x,y:Z) {(Zle_bool x y)=true}+{(Zle_bool y x)=true}.
 Proof.
   Intros. Unfold Zle_bool. Cut (Zcompare x y)=SUPERIEUR<->(Zcompare y x)=INFERIEUR.
   Case (Zcompare x y). Left . Reflexivity.
   Left . Reflexivity.
   Right . Rewrite (proj1 ? ? H (refl_equal ? ?)). Reflexivity.
   Apply Zcompare_ANTISYM.
-Qed.
+Defined.
 
 Lemma Zle_bool_plus_mono : (x,y,z,t:Z) (Zle_bool x y)=true -> (Zle_bool z t)=true ->
                                 (Zle_bool (Zplus x z) (Zplus y t))=true.
diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 04fc70f8a..fc0abca95 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -60,10 +60,10 @@ NewDestruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Qed.
 
-Lemma Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
+Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
 Proof.
 NewDestruct x;Auto with arith.
-Qed.
+Defined.
 
 Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)).
 NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.