1 files changed, 4 insertions, 184 deletions
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index 5aebcc55..8908175f 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -1,194 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Orders BinInt Zcompare Zorder ZOrderedType
- GenericMinMax.
-
-(** * Maximum and Minimum of two [Z] numbers *)
-
-Local Open Scope Z_scope.
-
-Unboxed Definition Zmax (n m:Z) :=
-  match n ?= m with
-    | Eq | Gt => n
-    | Lt => m
-  end.
-
-Unboxed Definition Zmin (n m:Z) :=
-  match n ?= m with
-    | Eq | Lt => n
-    | Gt => m
-  end.
-
-(** The functions [Zmax] and [Zmin] implement indeed
-    a maximum and a minimum *)
-
-Lemma Zmax_l : forall x y, y<=x -> Zmax x y = x.
-Proof.
- unfold Zle, Zmax. intros x y. rewrite <- (Zcompare_antisym x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmax_r : forall x y, x<=y -> Zmax x y = y.
-Proof.
- unfold Zle, Zmax. intros x y. generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmin_l : forall x y, x<=y -> Zmin x y = x.
-Proof.
- unfold Zle, Zmin. intros x y. generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmin_r : forall x y, y<=x -> Zmin x y = y.
-Proof.
- unfold Zle, Zmin. intros x y.
- rewrite <- (Zcompare_antisym x y). generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Module ZHasMinMax <: HasMinMax Z_as_OT.
- Definition max := Zmax.
- Definition min := Zmin.
- Definition max_l := Zmax_l.
- Definition max_r := Zmax_r.
- Definition min_l := Zmin_l.
- Definition min_r := Zmin_r.
-End ZHasMinMax.
-
-Module Z.
-
-(** We obtain hence all the generic properties of max and min. *)
-
-Include UsualMinMaxProperties Z_as_OT ZHasMinMax.
-
-(** * Properties specific to the [Z] domain *)
-
-(** 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.
+Require Import Orders BinInt Zcompare Zorder.
 
+(** THIS FILE IS DEPRECATED. *)
 
 (*begin hide*)
 (* Compatibility with names of the old Zminmax file *)
@@ -199,4 +19,4 @@ Notation Zmin_max_distr_r := Z.min_max_distr (only parsing).
 Notation Zmax_min_modular_r := Z.max_min_modular (only parsing).
 Notation Zmin_max_modular_r := Z.min_max_modular (only parsing).
 Notation max_min_disassoc := Z.max_min_disassoc (only parsing).
-(*end hide*)
-\ No newline at end of file
+(*end hide*)