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/Zmin.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'theories/ZArith/Zmin.v')
-rw-r--r-- | theories/ZArith/Zmin.v | 112 |
1 files changed, 68 insertions, 44 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index d48e62c5..d79ebe98 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -5,9 +5,12 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmin.v,v 1.3.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) +(*i $Id: Zmin.v 8032 2006-02-12 21:20:48Z herbelin $ i*) -(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(** 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 BinInt. @@ -17,23 +20,31 @@ Require Import Zorder. Open Local Scope Z_scope. (**********************************************************************) -(** Minimum on binary integer numbers *) +(** *** Minimum on binary integer numbers *) -Definition Zmin (n m:Z) := - match n ?= m return Z with - | Eq => n - | Lt => n +Unboxed Definition Zmin (n m:Z) := + match n ?= m with + | Eq | Lt => n | Gt => m end. -(** Properties of minimum on binary integer numbers *) +(** Characterization of the minimum on binary integer numbers *) -Lemma Zmin_SS : forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). +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; unfold Zmin in |- *; rewrite (Zcompare_succ_compat n m); - elim_compare n m; intros E; rewrite E; auto with arith. +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. + +(** 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; @@ -50,57 +61,70 @@ intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E; | apply Zle_refl ]. Qed. -Lemma Zmin_case : forall (n m:Z) (P:Z -> Set), P n -> P m -> P (Zmin n m). +Lemma Zmin_glb : forall n m p:Z, 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; apply Zmin_case; assumption. Qed. -Lemma Zmin_or : forall n m:Z, Zmin n m = n \/ Zmin n m = m. +(** Semi-lattice properties of min *) + +Lemma Zmin_idempotent : forall n:Z, Zmin n n = n. Proof. -unfold Zmin in |- *; intros; elim (n ?= m); auto. +unfold Zmin in |- *; intros; elim (n ?= n); auto. Qed. -Lemma Zmin_n_n : forall n:Z, Zmin n n = n. +Notation Zmin_n_n := Zmin_idempotent (only parsing). + +Lemma Zmin_comm : forall n m:Z, Zmin n m = Zmin m n. Proof. -unfold Zmin in |- *; intros; elim (n ?= n); 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_plus : forall n m p:Z, Zmin (n + p) (m + p) = Zmin n m + p. +Lemma Zmin_assoc : forall n m p:Z, Zmin n (Zmin m p) = Zmin (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 n m p; repeat apply Zmin_case_strong; intros; + reflexivity || (try apply Zle_antisym); eauto with zarith. Qed. -(**********************************************************************) -(** Maximum of two binary integer numbers *) +(** Additional properties of min *) -Definition Zmax a b := match a ?= b with - | Lt => b - | _ => a - end. +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. -(** Properties of maximum on binary integer numbers *) +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. -Ltac CaseEq name := - generalize (refl_equal name); pattern name at -1 in |- *; case name. +Notation Zmin_or := Zmin_irreducible (only parsing). -Theorem Zmax1 : forall a b, a <= Zmax a b. +Lemma Zmin_le_prime_inf : forall n m p:Z, Zmin n m <= p -> {n <= p} + {m <= p}. Proof. -intros a b; unfold Zmax in |- *; CaseEq (a ?= b); simpl in |- *; - auto with zarith. -unfold Zle in |- *; intros H; rewrite H; red in |- *; intros; discriminate. +intros n m p; apply Zmin_case; auto. Qed. -Theorem Zmax2 : forall a b, b <= Zmax a b. +(** Operations preserving min *) + +Lemma Zsucc_min_distr : + forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). Proof. -intros a b; unfold Zmax in |- *; CaseEq (a ?= b); simpl in |- *; - auto with zarith. -intros H; - (case (Zle_or_lt b a); auto; unfold Zlt in |- *; rewrite H; intros; - discriminate). -intros H; - (case (Zle_or_lt b a); auto; unfold Zlt in |- *; rewrite H; intros; - discriminate). +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. +Qed. + +Notation Zmin_plus := Zplus_min_distr_r (only parsing). |