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

1 files changed, 23 insertions, 14 deletions

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 *)