diff options
Diffstat (limited to 'theories/ZArith/Zmin.v')
| -rw-r--r-- | theories/ZArith/Zmin.v | 80 |
1 files changed, 40 insertions, 40 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index d79ebe98..37d78a74 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -5,126 +5,126 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmin.v 8032 2006-02-12 21:20:48Z herbelin $ i*) +(*i $Id: Zmin.v 9302 2006-10-27 21:21:17Z barras $ 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). *) -Require Import Arith. +Require Import Arith_base. Require Import BinInt. Require Import Zcompare. Require Import Zorder. Open Local Scope Z_scope. -(**********************************************************************) -(** *** Minimum on binary integer numbers *) +(**************************************) +(** Minimum on binary integer numbers *) Unboxed Definition Zmin (n m:Z) := match n ?= m with - | Eq | Lt => n - | Gt => m + | Eq | Lt => n + | Gt => m end. -(** Characterization of the minimum on binary integer numbers *) +(** * 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. + 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. + intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith. Qed. -(** Greatest lower bound properties of min *) +(** * 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 ]. + 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. 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 ]. + 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. Lemma Zmin_glb : forall n m p:Z, p <= n -> p <= m -> p <= Zmin n m. Proof. -intros; apply Zmin_case; assumption. + intros; apply Zmin_case; assumption. Qed. -(** Semi-lattice properties of min *) +(** * Semi-lattice properties of min *) Lemma Zmin_idempotent : forall n:Z, Zmin n n = n. Proof. -unfold Zmin in |- *; intros; elim (n ?= n); auto. + unfold Zmin in |- *; intros; elim (n ?= n); auto. Qed. 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. + 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. + intros n m p; repeat apply Zmin_case_strong; intros; + reflexivity || (try apply Zle_antisym); eauto with zarith. Qed. -(** Additional properties of min *) +(** * 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. + unfold Zmin in |- *; intros; elim (n ?= m); auto. 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. + intros n m; destruct (Zmin_irreducible_inf n m); [left|right]; trivial. 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. + intros n m p; apply Zmin_case; auto. Qed. -(** Operations preserving min *) +(** * 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. + intros n m; unfold Zmin in |- *; rewrite (Zcompare_succ_compat n m); + elim_compare n m; intros E; rewrite E; auto with arith. Qed. Notation Zmin_SS := Zsucc_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. + 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. Notation Zmin_plus := Zplus_min_distr_r (only parsing). |