aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zminmax.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-02-09 17:44:37 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-02-09 17:44:37 +0000
commit959b8555351fcf30bd747b47167dd0dca96d34c6 (patch)
treeaddfbecca5220e560e544d289fcf9c249aadeec8 /theories/ZArith/Zminmax.v
parent911c50439abdedd0f75856d43ff12e9615ec9980 (diff)
ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12714 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zminmax.v')
-rw-r--r--theories/ZArith/Zminmax.v62
1 files changed, 5 insertions, 57 deletions
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index c1657e298..70f72568f 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -6,69 +6,18 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Import Orders BinInt Zcompare Zorder ZOrderedType
- GenericMinMax.
+Require Import Orders BinInt Zcompare Zorder ZBinary.
(** * 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.
+(* All generic properties about max and min are already in [ZBinary.Z].
+ We prove here in addition some results specific to Z.
+*)
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 *)
+Include ZBinary.Z.
(** Compatibilities (consequences of monotonicity) *)
@@ -177,7 +126,6 @@ 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).