diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-23 16:35:26 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-23 16:35:26 +0000 |
commit | f3ddbcb8b977e9314ff5ef309bccfd17114f955c (patch) | |
tree | 0d29584d8c37c8f96ddabe2c940c6f6ff7a51ec6 /theories/ZArith/Zmin.v | |
parent | 485151f9ee054b0a0f390d4eff6a2bb2958ed8c2 (diff) |
cleanup of Zmin and Zmax
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zmin.v')
-rw-r--r-- | theories/ZArith/Zmin.v | 72 |
1 files changed, 36 insertions, 36 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 1f2de0c9f..2c5003a6d 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -10,83 +10,83 @@ Require Import BinInt Zcompare Zorder. -Open Local Scope Z_scope. +Local Open Scope Z_scope. -(** Definition [Zmin] is now [BinInt.Zmin]. *) +(** 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.add_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.add_min_distr_r (only parsing). (** * Minimum and Zpos *) -Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). +Lemma Zpos_min p q : Zpos (Pos.min p q) = Z.min (Zpos p) (Zpos q). Proof. - intros; unfold Zmin, Pmin; simpl. destruct Pos.compare; auto. + unfold Z.min, Pos.min; simpl. destruct Pos.compare; auto. Qed. -Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1. +Lemma Zpos_min_1 p : Z.min 1 (Zpos p) = 1. Proof. - intros; unfold Zmax; simpl; destruct p; simpl; auto. + now destruct p. Qed. |