diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/ZArith/Zmin.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/ZArith/Zmin.v')
-rw-r--r-- | theories/ZArith/Zmin.v | 106 |
1 files changed, 106 insertions, 0 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v new file mode 100644 index 00000000..d48e62c5 --- /dev/null +++ b/theories/ZArith/Zmin.v @@ -0,0 +1,106 @@ +(************************************************************************) +(* 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: Zmin.v,v 1.3.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) + +Require Import Arith. +Require Import BinInt. +Require Import Zcompare. +Require Import Zorder. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Minimum on binary integer numbers *) + +Definition Zmin (n m:Z) := + match n ?= m return Z with + | Eq => n + | Lt => n + | Gt => m + end. + +(** Properties of minimum on binary integer numbers *) + +Lemma Zmin_SS : 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. +Qed. + +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 ]. +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 ]. +Qed. + +Lemma Zmin_case : forall (n m:Z) (P:Z -> Set), 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. + +Lemma Zmin_or : forall n m:Z, Zmin n m = n \/ Zmin n m = m. +Proof. +unfold Zmin in |- *; intros; elim (n ?= m); auto. +Qed. + +Lemma Zmin_n_n : forall n:Z, Zmin n n = n. +Proof. +unfold Zmin in |- *; intros; elim (n ?= n); auto. +Qed. + +Lemma Zmin_plus : 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. + +(**********************************************************************) +(** Maximum of two binary integer numbers *) + +Definition Zmax a b := match a ?= b with + | Lt => b + | _ => a + end. + +(** Properties of maximum on binary integer numbers *) + +Ltac CaseEq name := + generalize (refl_equal name); pattern name at -1 in |- *; case name. + +Theorem Zmax1 : forall a b, a <= Zmax a b. +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. +Qed. + +Theorem Zmax2 : forall a b, b <= Zmax a b. +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). +Qed. |