Numbers: properties of min/max with respect to 0,S,P,add,sub,mul

 With these properties, we can kill Arith/MinMax, NArith/Nminmax,
 and leave ZArith/Zminmax as a compatibility file only. Now
 the instanciations NPeano.Nat, NBinary.N, ZBinary.Z, BigZ, BigN
 contains all theses facts.

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

6 files changed, 43 insertions, 157 deletions

diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index a263ab379..7a68bd511 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -22,6 +22,6 @@ Require Export Zlogarithm.
 
 Export ZArithRing.
 
-(** Final Z module, cumulating ZBinary.Z, Zminmax.Z, and Zdiv.Z *)
+(** Final Z module, cumulating ZBinary.Z and Zdiv.Z *)
 
 Module Z := Zdiv.Z.
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 1ce877b18..cd866c375 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -34,5 +34,3 @@ Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
   Zmult_plus_distr_r: zarith.
 
 Require Export Zhints.
-
-Module Z := Zminmax.Z.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 4477d559e..66e275b61 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -317,7 +317,7 @@ Module Z.
  Proof. intros; apply Z_mod_lt; auto with zarith. Qed.
  Definition mod_neg_bound := Z_mod_neg.
 
- Include ZBinary.Z (* ideally: Zminmax.Z *) <+ ZDivFloor.ZDivPropFunct.
+ Include ZBinary.Z <+ ZDivFloor.ZDivPropFunct.
 
 End Z.
 
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 84303a326..1d9b1f108 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -7,15 +7,13 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
+(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *)
 
-Require Export BinInt Zcompare Zorder Zminmax.
+Require Export BinInt Zcompare Zorder ZBinary.
 
 Open Local Scope Z_scope.
 
-(** [Zmax] is now [BinInt.Zmax]. Code that do things like
-  [unfold Zmax.Zmax] will have to be adapted, and neither
-  a [Definition] or a [Notation] here can help much. *)
+(** Definition [Zmax] is now [BinInt.Zmax]. *)
 
 
 (** * Characterization of maximum on binary integer numbers *)
@@ -78,24 +76,35 @@ Definition Zsucc_max_distr :
  := Z.succ_max_distr.
 
 Definition Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m
- := Z.plus_max_distr_l.
+ := Z.add_max_distr_l.
 
 Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p
- := Z.plus_max_distr_r.
+ := Z.add_max_distr_r.
 
 (** * Maximum and Zpos *)
 
-Definition Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q)
- := Z.pos_max.
+Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
+Proof.
+ intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
+ destruct Pcompare; auto.
+ intro H; rewrite H; auto.
+Qed.
 
-Definition Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p
- := Z.pos_max_1.
+Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
+Proof.
+  intros; unfold Zmax; simpl; destruct p; simpl; auto.
+Qed.
 
 (** * Characterization of Pminus in term of Zminus and Zmax *)
 
-Definition Zpos_minus :
- forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q)
- := Zpos_minus.
+Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
+Proof.
+  intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H.
+  rewrite (Pcompare_Eq_eq _ _ H).
+  unfold Pminus; rewrite Pminus_mask_diag; reflexivity.
+  rewrite Pminus_Lt; auto.
+  symmetry. apply Zpos_max_1.
+Qed.
 
 (* begin hide *)
 (* Compatibility *)
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 4703faace..e1599d943 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -7,16 +7,13 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
+(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *)
 
-Require Import BinInt Zcompare Zorder Zminmax.
+Require Import BinInt Zcompare Zorder ZBinary.
 
 Open Local Scope Z_scope.
 
-(** [Zmin] is now [BinInt.Zmin]. Code that do things like
-  [unfold Zmin.Zmin] will have to be adapted, and neither
-  a [Definition] or a [Notation] here can help much. *)
-
+(** Definition [Zmin] is now [BinInt.Zmin]. *)
 
 (** * Characterization of the minimum on binary integer numbers *)
 
@@ -77,14 +74,24 @@ Notation Zmin_SS := Z.succ_min_distr (only parsing).
 
 Definition Zplus_min_distr_r :
  forall n m p, Zmin (n + p) (m + p) = Zmin n m + p
- := Z.plus_min_distr_r.
+ := Z.add_min_distr_r.
 
-Notation Zmin_plus := Z.plus_min_distr_r (only parsing).
+Notation Zmin_plus := Z.add_min_distr_r (only parsing).
 
 (** * Minimum and Zpos *)
 
-Definition Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q)
- := Z.pos_min.
+Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
+Proof.
+ intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q).
+ destruct Pcompare; auto.
+Qed.
+
+Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1.
+Proof.
+  intros; unfold Zmax; simpl; destruct p; simpl; auto.
+Qed.
+
+
 
 
 
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index 70f72568f..3f2cd5a5f 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -8,135 +8,7 @@
 
 Require Import Orders BinInt Zcompare Zorder ZBinary.
 
-(** * Maximum and Minimum of two [Z] numbers *)
-
-Local Open Scope Z_scope.
-
-(* All generic properties about max and min are already in [ZBinary.Z].
-   We prove here in addition some results specific to Z.
-*)
-
-Module Z.
-Include ZBinary.Z.
-
-(** Compatibilities (consequences of monotonicity) *)
-
-Lemma plus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m.
-Proof.
- intros. apply max_monotone.
- intros x y. apply Zplus_le_compat_l.
-Qed.
-
-Lemma plus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p.
-Proof.
- intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p).
- apply plus_max_distr_l.
-Qed.
-
-Lemma plus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m.
-Proof.
- intros. apply Z.min_monotone.
- intros x y. apply Zplus_le_compat_l.
-Qed.
-
-Lemma plus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p.
-Proof.
- intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p).
- apply plus_min_distr_l.
-Qed.
-
-Lemma succ_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
-Proof.
- unfold Zsucc. intros. symmetry. apply plus_max_distr_r.
-Qed.
-
-Lemma succ_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
-Proof.
- unfold Zsucc. intros. symmetry. apply plus_min_distr_r.
-Qed.
-
-Lemma pred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m).
-Proof.
- unfold Zpred. intros. symmetry. apply plus_max_distr_r.
-Qed.
-
-Lemma pred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
-Proof.
- unfold Zpred. intros. symmetry. apply plus_min_distr_r.
-Qed.
-
-(** Anti-monotonicity swaps the role of [min] and [max] *)
-
-Lemma opp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m).
-Proof.
- intros. symmetry. apply min_max_antimonotone.
- intros x x'. red. red. rewrite <- Zcompare_opp; auto.
-Qed.
-
-Lemma opp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m).
-Proof.
- intros. symmetry. apply max_min_antimonotone.
- intros x x'. red. red. rewrite <- Zcompare_opp; auto.
-Qed.
-
-Lemma minus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m.
-Proof.
- unfold Zminus. intros. rewrite opp_min_distr. apply plus_max_distr_l.
-Qed.
-
-Lemma minus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p.
-Proof.
- unfold Zminus. intros. apply plus_max_distr_r.
-Qed.
-
-Lemma minus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m.
-Proof.
- unfold Zminus. intros. rewrite opp_max_distr. apply plus_min_distr_l.
-Qed.
-
-Lemma minus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p.
-Proof.
- unfold Zminus. intros. apply plus_min_distr_r.
-Qed.
-
-(** Compatibility with [Zpos] *)
-
-Lemma pos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
-Proof.
- intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
- destruct Pcompare; auto.
- intro H; rewrite H; auto.
-Qed.
-
-Lemma pos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
-Proof.
- intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q).
- destruct Pcompare; auto.
-Qed.
-
-Lemma pos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
-Proof.
-  intros; unfold Zmax; simpl; destruct p; simpl; auto.
-Qed.
-
-Lemma pos_min_1 : forall p, Zmin 1 (Zpos p) = 1.
-Proof.
-  intros; unfold Zmax; simpl; destruct p; simpl; auto.
-Qed.
-
-End Z.
-
-(** * Characterization of Pminus in term of Zminus and Zmax *)
-
-Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
-Proof.
-  intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H.
-  rewrite (Pcompare_Eq_eq _ _ H).
-  unfold Pminus; rewrite Pminus_mask_diag; reflexivity.
-  rewrite Pminus_Lt; auto.
-  symmetry. apply Z.pos_max_1.
-Qed.
-
+(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *)
 
 (*begin hide*)
 (* Compatibility with names of the old Zminmax file *)