Replaced BinNat with a new version that is based on theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers.

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

8 files changed, 173 insertions, 13 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 0e47356ada..e81cffe4f3 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NZAxioms.
 
 Set Implicit Arguments.
@@ -15,6 +27,10 @@ Notation P := NZpred.
 Notation Zplus := NZplus.
 Notation Ztimes := NZtimes.
 Notation Zminus := NZminus.
+Notation Zlt := NZlt.
+Notation Zle := NZle.
+Notation Zmin := NZmin.
+Notation Zmax := NZmax.
 Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
 Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
 Notation "0" := NZ0 : IntScope.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index dbe2aa4396..ace49428d2 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZAxioms.
 Require Import NZTimesOrder.
 
@@ -7,6 +19,12 @@ Open Local Scope IntScope.
 
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
+Theorem Zsucc_wd : forall n1 n2 : Z, n1 == n2 -> S n1 == S n2.
+Proof NZsucc_wd.
+
+Theorem Zpred_wd : forall n1 n2 : Z, n1 == n2 -> P n1 == P n2.
+Proof NZpred_wd.
+
 Theorem Zpred_succ : forall n : Z, P (S n) == n.
 Proof NZpred_succ.
 
@@ -22,6 +40,15 @@ Proof NZsucc_inj_wd.
 Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
+(* Decidability and stability of equality was proved only in NZOrder, but
+since it does not mention order, we'll put it here *)
+
+Theorem Zeq_em : forall n m : Z, n == m \/ n ~= m.
+Proof NZeq_em.
+
+Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m.
+Proof NZeq_dne.
+
 Theorem Zcentral_induction :
 forall A : Z -> Prop, predicate_wd Zeq A ->
   forall z : Z, A z ->
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 3146b9c2c3..51b522a52d 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export NumPrelude.
 
 Module Type ZDomainSignature.
@@ -6,14 +18,14 @@ Parameter Inline Z : Set.
 Parameter Inline Zeq : Z -> Z -> Prop.
 Parameter Inline e : Z -> Z -> bool.
 
-Axiom E_equiv_e : forall x y : Z, Zeq x y <-> e x y.
-Axiom E_equiv : equiv Z Zeq.
+Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y.
+Axiom eq_equiv : equiv Z Zeq.
 
 Add Relation Z Zeq
- reflexivity proved by (proj1 E_equiv)
- symmetry proved by (proj2 (proj2 E_equiv))
- transitivity proved by (proj1 (proj2 E_equiv))
-as E_rel.
+ reflexivity proved by (proj1 eq_equiv)
+ symmetry proved by (proj2 (proj2 eq_equiv))
+ transitivity proved by (proj1 (proj2 eq_equiv))
+as eq_rel.
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
@@ -29,12 +41,12 @@ Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
 Proof.
 intros x x' Exx' y y' Eyy'.
 case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
-assert (x == y); [apply <- E_equiv_e; now rewrite H2 |
+assert (x == y); [apply <- eq_equiv_e; now rewrite H2 |
 assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
-rewrite <- H1; assert (H3 : e x' y'); [now apply -> E_equiv_e | now inversion H3]]].
-assert (x' == y'); [apply <- E_equiv_e; now rewrite H1 |
+rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]].
+assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 |
 assert (x == y); [rewrite Exx'; now rewrite Eyy' |
-rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]].
+rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
 Qed.
 
 Theorem neq_symm : forall n m, n # m -> m # n.
@@ -50,7 +62,7 @@ Qed.
 Declare Left Step ZE_stepl.
 
 (* The right step lemma is just transitivity of Zeq *)
-Declare Right Step (proj1 (proj2 E_equiv)).
+Declare Right Step (proj1 (proj2 eq_equiv)).
 
 End ZDomainProperties.
 
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index 322d36cd3e..9b452039cb 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZTimes.
 
 Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
@@ -6,6 +18,22 @@ Open Local Scope IntScope.
 
 (* Axioms *)
 
+Theorem Zlt_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 < m1 <-> n2 < m2).
+Proof NZlt_wd.
+
+Theorem Zle_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
+Proof NZle_wd.
+
+Theorem Zmin_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmin n1 m1 == Zmin n2 m2.
+Proof NZmin_wd.
+
+Theorem Zmax_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2.
+Proof NZmax_wd.
+
 Theorem Zle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
 Proof NZle_lt_or_eq.
 
@@ -15,6 +43,18 @@ Proof NZlt_irrefl.
 Theorem Zlt_succ_le : forall n m : Z, n < S m <-> n <= m.
 Proof NZlt_succ_le.
 
+Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n.
+Proof NZmin_l.
+
+Theorem Zmin_r : forall n m : Z, m <= n -> Zmin n m == m.
+Proof NZmin_r.
+
+Theorem Zmax_l : forall n m : Z, m <= n -> Zmax n m == n.
+Proof NZmax_l.
+
+Theorem Zmax_r : forall n m : Z, n <= m -> Zmax n m == m.
+Proof NZmax_r.
+
 (* Renaming theorems from NZOrder.v *)
 
 Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m.
@@ -91,12 +131,18 @@ Proof NZle_antisymm.
 Theorem Zlt_trichotomy : forall n m : Z,  n < m \/ n == m \/ m < n.
 Proof NZlt_trichotomy.
 
+Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m.
+Proof NZlt_gt_cases.
+
 Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m.
 Proof NZle_gt_cases.
 
 Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m.
 Proof NZlt_ge_cases.
 
+Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m.
+Proof NZle_ge_cases.
+
 Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m.
 Proof NZle_ngt.
 
@@ -164,9 +210,9 @@ Proof NZright_induction'.
 Theorem Zleft_induction' :
   forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z,
-    (forall n : NZ, z <= n -> A n) ->
+    (forall n : Z, z <= n -> A n) ->
     (forall n : Z, n < z -> A (S n) -> A n) ->
-      forall n : NZ, A n.
+      forall n : Z, A n.
 Proof NZleft_induction'.
 
 Theorem Zstrong_right_induction :
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index bae74feca2..16fe114313 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -1,9 +1,25 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZBase.
 
 Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
+Theorem Zplus_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2.
+Proof NZplus_wd.
+
 Theorem Zplus_0_l : forall n : Z, 0 + n == n.
 Proof NZplus_0_l.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 49fd6f5588..01226b1218 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZOrder.
 
 Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 0290c237bb..14c59fcfa0 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export Ring.
 Require Export ZPlus.
 
@@ -5,6 +17,10 @@ Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
+Theorem Ztimes_wd :
+  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2.
+Proof NZtimes_wd.
+
 Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
 Proof NZtimes_0_r.
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index b1a0551f89..1b9e9b5192 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
 Require Export ZPlusOrder.
 
 Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
@@ -37,6 +49,9 @@ Proof NZtimes_le_mono_nonpos_r.
 Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof NZtimes_cancel_l.
 
+Theorem Ztimes_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m).
+Proof NZtimes_cancel_r.
+
 Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof NZtimes_le_mono_pos_l.