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

6 files changed, 263 insertions, 45 deletions

diff --git a/CHANGES b/CHANGES
index e6df48241..37afe0977 100644
--- a/CHANGES
+++ b/CHANGES
@@ -90,8 +90,9 @@ Notations
 
 Library
 
+- Small extension of Zmin.V, new Zmax.v, new Zminmax.v
 - New library on String and Ascii characters (contributed by L. Thery)
-- Few improvements in ZArith potentially exceptionally breaking the
+- Few other improvements in ZArith potentially exceptionally breaking the
   compatibility (useless hypothesys of Zgt_square_simpl and
   Zlt_square_simpl removed; fixed names mentioning letter O instead of
   digit 0; weaken premises in Z_lt_induction)
diff --git a/Makefile b/Makefile
index 476fa00f1..c5a7fdc6d 100644
--- a/Makefile
+++ b/Makefile
@@ -825,7 +825,8 @@ ZARITHVO=\
  theories/ZArith/auxiliary.vo   theories/ZArith/Zmisc.vo \
  theories/ZArith/Zcompare.vo    theories/ZArith/Znat.vo \
  theories/ZArith/Zorder.vo      theories/ZArith/Zabs.vo \
- theories/ZArith/Zmin.vo        theories/ZArith/Zeven.vo \
+ theories/ZArith/Zmin.vo        theories/ZArith/Zmax.vo \
+ theories/ZArith/Zminmax.vo     theories/ZArith/Zeven.vo \
  theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
  theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
  theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo \
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 2e7957848..767f9abc4 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -19,6 +19,8 @@ Require Export Zcompare.
 Require Export Zorder.
 Require Export Zeven.
 Require Export Zmin.
+Require Export Zmax.
+Require Export Zminmax.
 Require Export Zabs.
 Require Export Znat.
 Require Export auxiliary.
@@ -31,4 +33,4 @@ Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
   Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
   Zmult_plus_distr_r: zarith.
 
-Require Export Zhints.
\ No newline at end of file
+Require Export Zhints.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
new file mode 100644
index 000000000..4f6251551
--- /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$ 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.
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).
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
new file mode 100644
index 000000000..c311c7ce9
--- /dev/null
+++ b/theories/ZArith/Zminmax.v
@@ -0,0 +1,82 @@
+(************************************************************************)
+(*  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$ i*)
+
+Require Import Zmin Zmax.
+Require Import BinInt Zorder.
+
+Open Scope Z_scope.
+
+(** *** Lattice properties of min and max on Z *)
+
+(** Absorption *)
+
+Lemma Zmin_max_absorption_r_r : forall n m, Zmax n (Zmin n m) = n.
+Proof.
+intros; apply Zmin_case_strong; intro; apply Zmax_case_strong; intro; 
+  reflexivity || apply Zle_antisym; trivial.
+Qed.
+
+Lemma Zmax_min_absorption_r_r : forall n m, Zmin n (Zmax n m) = n.
+Proof.
+intros; apply Zmax_case_strong; intro; apply Zmin_case_strong; intro; 
+  reflexivity || apply Zle_antisym; trivial.
+Qed.
+
+(** Distributivity *)
+
+Lemma Zmax_min_distr_r : 
+  forall n m p, Zmax n (Zmin m p) = Zmin (Zmax n m) (Zmax n p).
+Proof.
+intros.
+repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; 
+  reflexivity ||
+  apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+Lemma Zmin_max_distr_r : 
+  forall n m p, Zmin n (Zmax m p) = Zmax (Zmin n m) (Zmin n p).
+Proof.
+intros.
+repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; 
+  reflexivity ||
+  apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+(** Modularity *)
+
+Lemma Zmax_min_modular_r :
+  forall n m p, Zmax n (Zmin m (Zmax n p)) = Zmin (Zmax n m) (Zmax n p).
+Proof.
+intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+  reflexivity ||
+  apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+Lemma Zmin_max_modular_r :
+  forall n m p, Zmin n (Zmax m (Zmin n p)) = Zmax (Zmin n m) (Zmin n p).
+Proof.
+intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+  reflexivity ||
+  apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+(** Disassociativity *)
+
+Lemma max_min_disassoc : forall n m p, Zmin n (Zmax m p) <= Zmax (Zmin n m) p.
+Proof.
+intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+  apply Zle_refl || (assumption || eapply Zle_trans; eassumption).
+Qed.
+
+
+
+
+
+
+