Some additions in Max and Zmax. Unifiying list of statements and names

in both files. Late update of CHANGES wrt classical Tauto.



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

3 files changed, 95 insertions, 33 deletions

diff --git a/CHANGES b/CHANGES
index d83ce42af4..eb4245bd1d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,8 @@ Tactics
 - Tactic "quote" now supports quotation of arbitrary terms (not just the
   goal).
 - Tactic "idtac" now displays its list arguments.
+- Tactic "tauto" now proves classical tautologies as soon as classical logic
+  (i.e. library Classical_Prop or Classical) is loaded.
 
 Vernacular commands
 
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 52beecb742..e43b804e56 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -8,13 +8,13 @@
 
 (*i $Id$ i*)
 
-Require Import Le.
+Require Import Le Plus.
 
 Open Local Scope nat_scope.
 
 Implicit Types m n : nat.
 
-(** * maximum of two natural numbers *)
+(** * Maximum of two natural numbers *)
 
 Fixpoint max n m {struct n} : nat :=
   match n, m with
@@ -23,64 +23,115 @@ Fixpoint max n m {struct n} : nat :=
     | S n', S m' => S (max n' m')
   end.
 
-(** * Simplifications of [max] *)
+(** * Inductive characterization of [max] *)
 
-Lemma max_SS : forall n m, S (max n m) = max (S n) (S m).
+Lemma max_case_strong : forall n m (P:nat -> Type), 
+  (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
 Proof.
-  auto with arith.
+  induction n; destruct m; simpl in *; auto with arith.
+  intros P H1 H2; apply IHn; intro; [apply H1|apply H2]; auto with arith.
 Qed.
 
-Theorem max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
+(** Propositional characterization of [max] *)
+
+Lemma max_spec : forall n m, m <= n /\ max n m = n \/ n <= m /\ max n m = m.
+Proof.
+  intros n m; apply max_case_strong; auto.
+Qed.
+
+(** * [max n m] is equal to [n] or [m] *)
+
+Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
+Proof.
+  induction n; destruct m; simpl; auto.
+  destruct (IHn m) as [-> | ->]; auto.
+Defined.
+
+(** [max n m] is equal to [n] or [m], alternative formulation *)
+
+Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
+Proof.
+  intros n m; destruct (max_dec n m) as [-> | ->]; auto.
+Defined.
+
+(** * Compatibility properties of [max] *)
+
+Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m).
+Proof.
+  auto.
+Qed.
+
+Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m.
+Proof.
+  induction p; simpl; auto. 
+Qed.
+
+Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p.
+Proof.
+  intros n m p; repeat rewrite (plus_comm _ p).
+  apply plus_max_distr_l.
+Qed.
+
+(** * Semi-lattice algebraic properties of [max] *)
+
+Lemma max_idempotent : forall n, max n n = n.
+Proof.
+  intros; apply max_case; auto.
+Qed.
+
+Lemma max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
 Proof.
   induction m; destruct n; destruct p; trivial.
-  simpl.
-  auto using IHm.
+  simpl; auto.
 Qed.
 
 Lemma max_comm : forall n m, max n m = max m n.
 Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
+  induction n; destruct m; simpl; auto.
 Qed.
 
-(** * [max] and [le] *)
+(** * Least-upper bound properties of [max] *)
 
 Lemma max_l : forall n m, m <= n -> max n m = n.
 Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
+  induction n; destruct m; simpl; auto with arith.
 Qed.
 
 Lemma max_r : forall n m, n <= m -> max n m = m.
 Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
+  induction n; destruct m; simpl; auto with arith.
 Qed.
 
 Lemma le_max_l : forall n m, n <= max n m.
 Proof.
-  induction n; intros; simpl in |- *; auto with arith.
-  elim m; intros; simpl in |- *; auto with arith.
+  induction n; simpl; auto with arith.
+  destruct m; simpl; auto with arith.
 Qed.
 
 Lemma le_max_r : forall n m, m <= max n m.
 Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; simpl in |- *; auto with arith.
+  induction n; simpl; auto with arith.
+  induction m; simpl; auto with arith.
 Qed.
 Hint Resolve max_r max_l le_max_l le_max_r: arith v62.
 
+Lemma max_lub_l : forall n m p, max n m <= p -> n <= p.
+Proof.
+intros n m p; eapply le_trans. apply le_max_l.
+Qed.
 
-(** * [max n m] is equal to [n] or [m] *)
-
-Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
+Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
 Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-  elim (IHn m); intro H; elim H; auto.
-Defined.
+intros n m p; eapply le_trans. apply le_max_r.
+Qed.
 
-Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
+Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p.
 Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; intros; simpl in |- *; auto with arith.
-  pattern (max n m) in |- *; apply IHn; auto with arith.
-Defined.
+  intros n m p; apply max_case; auto.
+Qed.
 
+(* begin hide *)
+(* Compatibility *)
 Notation max_case2 := max_case (only parsing).
+Notation max_SS := succ_max_distr (only parsing).
+(* end hide *)
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index c21b4affb8..59fcfa4947 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -102,12 +102,12 @@ Qed.
 
 (** * Additional properties of max *)
 
-Lemma Zmax_irreducible_inf : forall n m:Z, Zmax n m = n \/ Zmax n m = m.
+Lemma Zmax_irreducible_dec : 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.
+Lemma Zmax_le_prime : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m.
 Proof.
   intros n m p; apply Zmax_case; auto.
 Qed.
@@ -121,12 +121,16 @@ Proof.
     elim_compare n m; intros E; rewrite E; auto with arith.
 Qed.
 
+Lemma Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m.
+Proof.
+  intros n m p; unfold Zmax.
+  rewrite (Zcompare_plus_compat n m p).
+  destruct (n ?= m); trivial.
+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.
+  intros n m p; repeat rewrite (Zplus_comm _ p); apply Zplus_max_distr_l.
 Qed.
 
 (** * Maximum and Zpos *)
@@ -164,3 +168,8 @@ Proof.
   symmetry; apply Zpos_max_1.
 Qed.
 
+(* begin hide *)
+(* Compatibility *)
+Notation Zmax_irreducible_inf := Zmax_irreducible_dec (only parsing).
+Notation Zmax_le_prime_inf := Zmax_le_prime (only parsing).
+(* end hide *)