diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /theories/ZArith/Zmax.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'theories/ZArith/Zmax.v')
-rw-r--r-- | theories/ZArith/Zmax.v | 108 |
1 files changed, 108 insertions, 0 deletions
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v new file mode 100644 index 00000000..ae3bbf41 --- /dev/null +++ b/theories/ZArith/Zmax.v @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * 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*) + +Require Import Arith. +Require Import BinInt. +Require Import Zcompare. +Require Import Zorder. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** *** Maximum of two binary integer numbers *) + +Definition Zmax m n := + match m ?= n with + | Eq | Gt => m + | Lt => n + end. + +(** 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. +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. +Qed. + +(** 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. +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. +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. +Qed. + +(** Semi-lattice properties of max *) + +Lemma Zmax_idempotent : forall n:Z, Zmax n n = n. +Proof. +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. +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. +Qed. + +(** 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. +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. +Qed. + +(** 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. +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. +Qed. |