diff options
Diffstat (limited to 'theories/ZArith/Zmax.v')
| -rw-r--r-- | theories/ZArith/Zmax.v | 62 |
1 files changed, 31 insertions, 31 deletions
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index ae3bbf41..8af9b891 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -5,104 +5,104 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmax.v 8032 2006-02-12 21:20:48Z herbelin $ i*) +(*i $Id: Zmax.v 9302 2006-10-27 21:21:17Z barras $ i*) -Require Import Arith. +Require Import Arith_base. Require Import BinInt. Require Import Zcompare. Require Import Zorder. Open Local Scope Z_scope. -(**********************************************************************) -(** *** Maximum of two binary integer numbers *) +(******************************************) +(** Maximum of two binary integer numbers *) Definition Zmax m n := - match m ?= n with + match m ?= n with | Eq | Gt => m | Lt => n - end. + end. -(** Characterization of maximum on binary integer numbers *) +(** * Characterization of maximum on binary integer numbers *) Lemma Zmax_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmax n m). Proof. -intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith. + intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith. Qed. Lemma Zmax_case_strong : forall (n m:Z) (P:Z -> Type), (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m). Proof. -intros n m P H1 H2; unfold Zmax, Zle, Zge in *. -rewrite <- (Zcompare_antisym n m) in H1. -destruct (n ?= m); (apply H1|| apply H2); discriminate. + intros n m P H1 H2; unfold Zmax, Zle, Zge in *. + rewrite <- (Zcompare_antisym n m) in H1. + destruct (n ?= m); (apply H1|| apply H2); discriminate. Qed. -(** Least upper bound properties of max *) +(** * Least upper bound properties of max *) Lemma Zle_max_l : forall n m:Z, n <= Zmax n m. Proof. -intros; apply Zmax_case_strong; auto with zarith. + intros; apply Zmax_case_strong; auto with zarith. Qed. Notation Zmax1 := Zle_max_l (only parsing). Lemma Zle_max_r : forall n m:Z, m <= Zmax n m. Proof. -intros; apply Zmax_case_strong; auto with zarith. + intros; apply Zmax_case_strong; auto with zarith. Qed. Notation Zmax2 := Zle_max_r (only parsing). Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p. Proof. -intros; apply Zmax_case; assumption. + intros; apply Zmax_case; assumption. Qed. -(** Semi-lattice properties of max *) +(** * Semi-lattice properties of max *) Lemma Zmax_idempotent : forall n:Z, Zmax n n = n. Proof. -intros; apply Zmax_case; auto. + intros; apply Zmax_case; auto. Qed. Lemma Zmax_comm : forall n m:Z, Zmax n m = Zmax m n. Proof. -intros; do 2 apply Zmax_case_strong; intros; - apply Zle_antisym; auto with zarith. + intros; do 2 apply Zmax_case_strong; intros; + apply Zle_antisym; auto with zarith. Qed. Lemma Zmax_assoc : forall n m p:Z, Zmax n (Zmax m p) = Zmax (Zmax n m) p. Proof. -intros n m p; repeat apply Zmax_case_strong; intros; - reflexivity || (try apply Zle_antisym); eauto with zarith. + intros n m p; repeat apply Zmax_case_strong; intros; + reflexivity || (try apply Zle_antisym); eauto with zarith. Qed. -(** Additional properties of max *) +(** * Additional properties of max *) Lemma Zmax_irreducible_inf : forall n m:Z, Zmax n m = n \/ Zmax n m = m. Proof. -intros; apply Zmax_case; auto. + intros; apply Zmax_case; auto. Qed. Lemma Zmax_le_prime_inf : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m. Proof. -intros n m p; apply Zmax_case; auto. + intros n m p; apply Zmax_case; auto. Qed. -(** Operations preserving max *) +(** * Operations preserving max *) Lemma Zsucc_max_distr : forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m). Proof. -intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m); - elim_compare n m; intros E; rewrite E; auto with arith. + intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m); + elim_compare n m; intros E; rewrite E; auto with arith. Qed. Lemma Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p. Proof. -intros x y n; unfold Zmax 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 Zmax 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. |