Nettoyage Zmin.v, création Zmax.v et Zminmax.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8032 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 66 insertions, 42 deletions

diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index d7ebad149..79f2154c3 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -7,7 +7,10 @@
 (************************************************************************)
 (*i $Id$ 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 *)
 
 Unboxed Definition Zmin (n m:Z) :=
-  match n ?= m return Z with
-  | Eq => n
-  | Lt => n
+  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).