diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-09 07:59:19 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-09 07:59:19 +0000 |
| commit | df9a4f1ae642cbbd2a6f1a3b82ad8169b7ec5ae6 (patch) | |
| tree | 47f00369a7e6ceef22bdd4ab7406091b58108924 /theories/ZArith/Zmisc.v | |
| parent | c04fe01b5d33b5e091c8fd19047514a7e4c4f311 (diff) | |
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
Diffstat (limited to 'theories/ZArith/Zmisc.v')
| -rw-r--r-- | theories/ZArith/Zmisc.v | 16 |
1 files changed, 8 insertions, 8 deletions
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. |