ZArith_base, Zbool, Bool_nat

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

1 files changed, 38 insertions, 0 deletions

diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
new file mode 100644
index 000000000..872c314f1
--- /dev/null
+++ b/theories/Arith/Bool_nat.v
@@ -0,0 +1,38 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require Export Compare_dec.
+Require Export Peano_dec.
+Require Sumbool.
+
+(** The decidability of equality and order relations over
+    type [nat] give some boolean functions with the adequate specification. *)
+
+Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)).
+Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} := 
+  [n,m:nat] (sumbool_not ? ? (le_lt_dec m n)).
+
+Definition nat_lt_ge_bool := 
+  [x,y:nat](bool_of_sumbool (lt_ge_dec x y)).
+Definition nat_ge_lt_bool := 
+  [x,y:nat](bool_of_sumbool (sumbool_not ? ? (lt_ge_dec x y))).
+
+Definition nat_le_gt_bool := 
+  [x,y:nat](bool_of_sumbool (le_gt_dec x y)).
+Definition nat_gt_le_bool := 
+  [x,y:nat](bool_of_sumbool (sumbool_not ? ? (le_gt_dec x y))).
+
+Definition nat_eq_bool :=
+  [x,y:nat](bool_of_sumbool (eq_nat_dec x y)).
+Definition nat_noteq_bool := 
+  [x,y:nat](bool_of_sumbool (sumbool_not ? ? (eq_nat_dec x y))).
+
+Definition zerop_bool := [x:nat](bool_of_sumbool (zerop x)).
+Definition notzerop_bool := [x:nat](bool_of_sumbool (notzerop x)).