summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zmin.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/ZArith/Zmin.v
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/ZArith/Zmin.v')
-rw-r--r--theories/ZArith/Zmin.v89
1 files changed, 47 insertions, 42 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 7b9ad469..2c5003a6 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -1,90 +1,95 @@
(************************************************************************)
(* 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 *)
(************************************************************************)
-(*i $Id: Zmin.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
+(** THIS FILE IS DEPRECATED. *)
-Require Import BinInt Zorder Zminmax.
+Require Import BinInt Zcompare Zorder.
-Open Local Scope Z_scope.
-
-(** [Zmin] is now [Zminmax.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. *)
+Local Open Scope Z_scope.
+(** Definition [Zmin] is now [BinInt.Z.min]. *)
(** * Characterization of the minimum on binary integer numbers *)
Definition Zmin_case := Z.min_case.
Definition Zmin_case_strong := Z.min_case_strong.
-Lemma Zmin_spec : forall x y,
- x <= y /\ Zmin x y = x \/ x > y /\ Zmin x y = y.
+Lemma Zmin_spec x y :
+ x <= y /\ Z.min x y = x \/ x > y /\ Z.min x y = y.
Proof.
- intros x y. rewrite Zgt_iff_lt, Z.min_comm. destruct (Z.min_spec y x); auto.
+ Z.swap_greater. rewrite Z.min_comm. destruct (Z.min_spec y x); auto.
Qed.
(** * Greatest lower bound properties of min *)
-Definition Zle_min_l : forall n m, Zmin n m <= n := Z.le_min_l.
-Definition Zle_min_r : forall n m, Zmin n m <= m := Z.le_min_r.
+Lemma Zle_min_l : forall n m, Z.min n m <= n. Proof Z.le_min_l.
+Lemma Zle_min_r : forall n m, Z.min n m <= m. Proof Z.le_min_r.
-Definition Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Zmin n m
- := Z.min_glb.
-Definition Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Zmin n m
- := Z.min_glb_lt.
+Lemma Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Z.min n m.
+Proof Z.min_glb.
+Lemma Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Z.min n m.
+Proof Z.min_glb_lt.
(** * Compatibility with order *)
-Definition Zle_min_compat_r : forall n m p, n <= m -> Zmin n p <= Zmin m p
- := Z.min_le_compat_r.
-Definition Zle_min_compat_l : forall n m p, n <= m -> Zmin p n <= Zmin p m
- := Z.min_le_compat_l.
+Lemma Zle_min_compat_r : forall n m p, n <= m -> Z.min n p <= Z.min m p.
+Proof Z.min_le_compat_r.
+Lemma Zle_min_compat_l : forall n m p, n <= m -> Z.min p n <= Z.min p m.
+Proof Z.min_le_compat_l.
(** * Semi-lattice properties of min *)
-Definition Zmin_idempotent : forall n, Zmin n n = n := Z.min_id.
-Notation Zmin_n_n := Zmin_idempotent (only parsing).
-Definition Zmin_comm : forall n m, Zmin n m = Zmin m n := Z.min_comm.
-Definition Zmin_assoc : forall n m p, Zmin n (Zmin m p) = Zmin (Zmin n m) p
- := Z.min_assoc.
+Lemma Zmin_idempotent : forall n, Z.min n n = n. Proof Z.min_id.
+Notation Zmin_n_n := Z.min_id (only parsing).
+Lemma Zmin_comm : forall n m, Z.min n m = Z.min m n. Proof Z.min_comm.
+Lemma Zmin_assoc : forall n m p, Z.min n (Z.min m p) = Z.min (Z.min n m) p.
+Proof Z.min_assoc.
(** * Additional properties of min *)
-Lemma Zmin_irreducible_inf : forall n m, {Zmin n m = n} + {Zmin n m = m}.
-Proof. exact Z.min_dec. Qed.
+Lemma Zmin_irreducible_inf : forall n m, {Z.min n m = n} + {Z.min n m = m}.
+Proof Z.min_dec.
-Lemma Zmin_irreducible : forall n m, Zmin n m = n \/ Zmin n m = m.
-Proof. intros; destruct (Z.min_dec n m); auto. Qed.
+Lemma Zmin_irreducible n m : Z.min n m = n \/ Z.min n m = m.
+Proof. destruct (Z.min_dec n m); auto. Qed.
Notation Zmin_or := Zmin_irreducible (only parsing).
-Lemma Zmin_le_prime_inf : forall n m p, Zmin n m <= p -> {n <= p} + {m <= p}.
-Proof. intros n m p; apply Zmin_case; auto. Qed.
+Lemma Zmin_le_prime_inf n m p : Z.min n m <= p -> {n <= p} + {m <= p}.
+Proof. apply Zmin_case; auto. Qed.
(** * Operations preserving min *)
-Definition Zsucc_min_distr :
- forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m)
- := Z.succ_min_distr.
+Lemma Zsucc_min_distr :
+ forall n m, Z.succ (Z.min n m) = Z.min (Z.succ n) (Z.succ m).
+Proof Z.succ_min_distr.
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.
+Lemma Zplus_min_distr_r :
+ forall n m p, Z.min (n + p) (m + p) = Z.min n m + p.
+Proof 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 p q : Zpos (Pos.min p q) = Z.min (Zpos p) (Zpos q).
+Proof.
+ unfold Z.min, Pos.min; simpl. destruct Pos.compare; auto.
+Qed.
+
+Lemma Zpos_min_1 p : Z.min 1 (Zpos p) = 1.
+Proof.
+ now destruct p.
+Qed.
+
+