diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-05 13:43:45 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-05 13:43:45 +0000 |
commit | b1e1be15990aef3fd76b28fad3d52cf6bc36a60b (patch) | |
tree | d9d4944e0cd7267e99583405a63b6f72c53f6182 /theories/ZArith/Zmin.v | |
parent | 380a8c4a8e7fb56fa105a76694f60f262d27d1a1 (diff) |
Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de la partie Omega dans contrib/omega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zmin.v')
-rw-r--r-- | theories/ZArith/Zmin.v | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v new file mode 100644 index 000000000..b09299466 --- /dev/null +++ b/theories/ZArith/Zmin.v @@ -0,0 +1,74 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(*i $Id$ i*) + +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) + +Require Arith. +Require fast_integer. +Require Zorder. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Minimum on binary integer numbers *) + +Definition Zmin := [n,m:Z] + <Z>Cases (Zcompare n m) of + EGAL => n + | INFERIEUR => n + | SUPERIEUR => m + end. + +(** Properties of minimum on binary integer numbers *) + +Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))). +Proof. +Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m); +(ElimCompare 'n 'm);Intros E;Rewrite E;Auto with arith. +Qed. + +Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n). +Proof. +Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E; + [ Apply Zle_n | Apply Zle_n | Apply Zlt_le_weak; Apply Zgt_lt;Exact E ]. +Qed. + +Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m). +Proof. +Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E;[ + Unfold Zle ;Rewrite -> E;Discriminate +| Unfold Zle ;Rewrite -> E;Discriminate +| Apply Zle_n ]. +Qed. + +Lemma Zmin_case : (n,m:Z)(P:Z->Set)(P n)->(P m)->(P (Zmin n m)). +Proof. +Intros n m P H1 H2; Unfold Zmin; Case (Zcompare n m);Auto with arith. +Qed. + +Lemma Zmin_or : (n,m:Z)(Zmin n m)=n \/ (Zmin n m)=m. +Proof. +Unfold Zmin; Intros; Elim (Zcompare n m); Auto. +Qed. + +Lemma Zmin_n_n : (n:Z) (Zmin n n)=n. +Proof. +Unfold Zmin; Intros; Elim (Zcompare n n); Auto. +Qed. + +Lemma Zmin_plus : + (x,y,n:Z)(Zmin (Zplus x n) (Zplus y n))=(Zplus (Zmin x y) n). +Proof. +Intros; Unfold Zmin. +Rewrite (Zplus_sym x n); +Rewrite (Zplus_sym y n); +Rewrite (Zcompare_Zplus_compatible x y n). +Case (Zcompare x y); Apply Zplus_sym. +Qed. + |