Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibniz part

 Moreover, instantiation like MinMax are now made without redefining
 generic properties (easier maintenance). We start using inner modules
 for qualifying (e.g. Z.max_comm).

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

1 files changed, 19 insertions, 19 deletions

diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index e6582a775..53c40ae7d 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -20,13 +20,13 @@ Open Local Scope Z_scope.
 
 (** * Characterization of maximum on binary integer numbers *)
 
-Definition Zmax_case := Zmax_case.
-Definition Zmax_case_strong := Zmax_case_strong.
+Definition Zmax_case := Z.max_case.
+Definition Zmax_case_strong := Z.max_case_strong.
 
 Lemma Zmax_spec : forall x y,
   x >= y /\ Zmax x y = x  \/ x < y /\ Zmax x y = y.
 Proof.
- intros x y. rewrite Zge_iff_le. destruct (Zmax_spec x y); auto.
+ intros x y. rewrite Zge_iff_le. destruct (Z.max_spec x y); auto.
 Qed.
 
 Lemma Zmax_left : forall n m, n>=m -> Zmax n m = n.
@@ -36,60 +36,60 @@ Definition Zmax_right : forall n m, n<=m -> Zmax n m = m := Zmax_r.
 
 (** * Least upper bound properties of max *)
 
-Definition Zle_max_l : forall n m, n <= Zmax n m := Zle_max_l.
-Definition Zle_max_r : forall n m, m <= Zmax n m := Zle_max_r.
+Definition Zle_max_l : forall n m, n <= Zmax n m := Z.le_max_l.
+Definition Zle_max_r : forall n m, m <= Zmax n m := Z.le_max_r.
 
 Definition Zmax_lub : forall n m p, n <= p -> m <= p -> Zmax n m <= p
- := Zmax_lub.
+ := Z.max_lub.
 
 Definition Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Zmax n m < p
- := Zmax_lub_lt.
+ := Z.max_lub_lt.
 
 
 (** * Compatibility with order *)
 
 Definition Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p
- := Zmax_le_compat_r.
+ := Z.max_le_compat_r.
 
 Definition Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m
- := Zmax_le_compat_l.
+ := Z.max_le_compat_l.
 
 
 (** * Semi-lattice properties of max *)
 
-Definition Zmax_idempotent : forall n, Zmax n n = n := Zmax_id.
-Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Zmax_comm.
+Definition Zmax_idempotent : forall n, Zmax n n = n := Z.max_id.
+Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Z.max_comm.
 Definition Zmax_assoc : forall n m p, Zmax n (Zmax m p) = Zmax (Zmax n m) p
- := Zmax_assoc.
+ := Z.max_assoc.
 
 (** * Additional properties of max *)
 
 Lemma Zmax_irreducible_dec : forall n m, {Zmax n m = n} + {Zmax n m = m}.
-Proof. exact Zmax_dec. Qed.
+Proof. exact Z.max_dec. Qed.
 
 Definition Zmax_le_prime : forall n m p, p <= Zmax n m -> p <= n \/ p <= m
- := Zmax_le.
+ := Z.max_le.
 
 
 (** * Operations preserving max *)
 
 Definition Zsucc_max_distr :
   forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m)
- := 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
- := Zplus_max_distr_l.
+ := Z.plus_max_distr_l.
 
 Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p
- := Zplus_max_distr_r.
+ := Z.plus_max_distr_r.
 
 (** * Maximum and Zpos *)
 
 Definition Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q)
- := Zpos_max.
+ := Z.pos_max.
 
 Definition Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p
- := Zpos_max_1.
+ := Z.pos_max_1.
 
 (** * Characterization of Pminus in term of Zminus and Zmax *)