summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zmin.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zmin.v')
-rw-r--r--theories/ZArith/Zmin.v146
1 files changed, 45 insertions, 101 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index bad40a32..5dd26fa3 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -5,142 +5,86 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zmin.v 10028 2007-07-18 22:38:06Z letouzey $ i*)
+(*i $Id$ i*)
-(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
- Further extensions by the Coq development team, with suggestions
- from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
- *)
+(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
-Require Import Arith_base.
-Require Import BinInt.
-Require Import Zcompare.
-Require Import Zorder.
+Require Import BinInt Zorder Zminmax.
Open Local Scope Z_scope.
-(**************************************)
-(** Minimum on binary integer numbers *)
+(** [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. *)
-Unboxed Definition Zmin (n m:Z) :=
- match n ?= m with
- | Eq | Lt => n
- | Gt => m
- end.
(** * Characterization of the minimum on binary integer numbers *)
-Lemma Zmin_case_strong : forall (n m:Z) (P:Z -> Type),
- (n<=m -> P n) -> (m<=n -> P m) -> P (Zmin n m).
-Proof.
- intros n m P H1 H2; unfold Zmin, Zle, Zge in *.
- rewrite <- (Zcompare_antisym n m) in H2.
- destruct (n ?= m); (apply H1|| apply H2); discriminate.
-Qed.
-
-Lemma Zmin_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmin n m).
-Proof.
- intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith.
-Qed.
+Definition Zmin_case := Z.min_case.
+Definition Zmin_case_strong := Z.min_case_strong.
-Lemma Zmin_spec : forall x y:Z,
- x <= y /\ Zmin x y = x \/
- x > y /\ Zmin x y = y.
+Lemma Zmin_spec : forall x y,
+ x <= y /\ Zmin x y = x \/ x > y /\ Zmin x y = y.
Proof.
- intros; unfold Zmin, Zle, Zgt.
- destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate.
+ intros x y. rewrite Zgt_iff_lt, Z.min_comm. destruct (Z.min_spec y x); auto.
Qed.
(** * Greatest lower bound properties of min *)
-Lemma Zle_min_l : forall n m:Z, Zmin n m <= n.
-Proof.
- intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E;
- [ apply Zle_refl
- | apply Zle_refl
- | apply Zlt_le_weak; apply Zgt_lt; exact E ].
-Qed.
+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_r : forall n m:Z, Zmin n m <= m.
-Proof.
- intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E;
- [ unfold Zle in |- *; rewrite E; discriminate
- | unfold Zle in |- *; rewrite E; discriminate
- | apply Zle_refl ].
-Qed.
+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:Z, p <= n -> p <= m -> p <= Zmin n m.
-Proof.
- intros; apply Zmin_case; assumption.
-Qed.
+(** * Compatibility with order *)
-(** * Semi-lattice properties of min *)
+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 Zmin_idempotent : forall n:Z, Zmin n n = n.
-Proof.
- unfold Zmin in |- *; intros; elim (n ?= n); auto.
-Qed.
+(** * 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).
-
-Lemma Zmin_comm : forall n m:Z, Zmin n m = Zmin m n.
-Proof.
- intros n m; unfold Zmin.
- rewrite <- (Zcompare_antisym n m).
- assert (H:=Zcompare_Eq_eq n m).
- destruct (n ?= m); simpl; auto.
-Qed.
-
-Lemma Zmin_assoc : forall n m p:Z, Zmin n (Zmin m p) = Zmin (Zmin n m) p.
-Proof.
- intros n m p; repeat apply Zmin_case_strong; intros;
- reflexivity || (try apply Zle_antisym); eauto with zarith.
-Qed.
+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.
(** * Additional properties of min *)
-Lemma Zmin_irreducible_inf : forall n m:Z, {Zmin n m = n} + {Zmin n m = m}.
-Proof.
- unfold Zmin in |- *; intros; elim (n ?= m); auto.
-Qed.
+Lemma Zmin_irreducible_inf : forall n m, {Zmin n m = n} + {Zmin n m = m}.
+Proof. exact Z.min_dec. Qed.
-Lemma Zmin_irreducible : forall n m:Z, Zmin n m = n \/ Zmin n m = m.
-Proof.
- intros n m; destruct (Zmin_irreducible_inf n m); [left|right]; trivial.
-Qed.
+Lemma Zmin_irreducible : forall n m, Zmin n m = n \/ Zmin n m = m.
+Proof. intros; destruct (Z.min_dec n m); auto. Qed.
Notation Zmin_or := Zmin_irreducible (only parsing).
-Lemma Zmin_le_prime_inf : forall n m p:Z, Zmin n m <= p -> {n <= p} + {m <= p}.
-Proof.
- intros n m p; apply Zmin_case; auto.
-Qed.
+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.
(** * Operations preserving min *)
-Lemma Zsucc_min_distr :
- forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
-Proof.
- intros n m; unfold Zmin in |- *; rewrite (Zcompare_succ_compat n m);
- elim_compare n m; intros E; rewrite E; auto with arith.
-Qed.
+Definition Zsucc_min_distr :
+ forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m)
+ := Z.succ_min_distr.
-Notation Zmin_SS := Zsucc_min_distr (only parsing).
+Notation Zmin_SS := Z.succ_min_distr (only parsing).
-Lemma Zplus_min_distr_r : forall n m p:Z, Zmin (n + p) (m + p) = Zmin n m + p.
-Proof.
- intros x y n; unfold Zmin in |- *.
- rewrite (Zplus_comm x n); rewrite (Zplus_comm y n);
- rewrite (Zcompare_plus_compat x y n).
- case (x ?= y); apply Zplus_comm.
-Qed.
+Definition Zplus_min_distr_r :
+ forall n m p, Zmin (n + p) (m + p) = Zmin n m + p
+ := Z.plus_min_distr_r.
-Notation Zmin_plus := Zplus_min_distr_r (only parsing).
+Notation Zmin_plus := Z.plus_min_distr_r (only parsing).
(** * Minimum and Zpos *)
-Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
-Proof.
- intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto.
-Qed.
+Definition Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q)
+ := Z.pos_min.
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 17:10:30 +0000