Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).

- tauto/intuition now works uniformly on and, prod, or, sum, False,
  Empty_set, unit, True (and isomorphic copies of them), iff, ->, and
  on all inhabited singleton types with a no-arguments constructor
  such as "eq t t" (even though the last case goes out of
  propositional logic: this features is so often used that it is
  difficult to come back on it).
- New dtauto and dintuition works on all inductive types with one
  constructors and no real arguments (for instance, they work on
  records such as "Equivalence"), in addition to -> and eq-like types.
- Moreover, both of them no longer unfold inner negations (this is a
  souce of incompatibility for intuition and evaluation of the level
  of incompatibility on contribs still needs to be done).

Incidentally, and amazingly, fixing bug #2680 made that constants
InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto
had indeed destructed a section hypothesis "@StrictOrder A ltA@
thinking it was a conjunction, making this section hypothesis
artificially necessary while it was not.

Renouncing to the unfolding of inner negations made auto/eauto
sometimes succeeding more, sometimes succeeding less. There is by the
way a (standard) problem with not in auto/eauto: even when given as an
"unfold hint", it works only in goals, not in hypotheses, so that auto
is not able to solve something like "forall P, (forall x, ~ P x) -> P
0 -> False". Should we automatically add a lemma of type "HYPS -> A ->
False" in the hint database everytime a lemma ""HYPS -> ~A" is
declared (and "unfold not" is a hint), and similarly for all unfold
hints?

At this occasion, also re-did some proofs of Znumtheory.

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

1 files changed, 22 insertions, 24 deletions

diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 6eb1a7093..2d4bfb2e3 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -575,30 +575,29 @@ Lemma prime_divisors :
   forall p:Z,
     prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.
 Proof.
-  simple induction 1; intros.
+  destruct 1; intros.
   assert
     (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p).
-  assert (Zabs a <= Zabs p). apply Zdivide_bounds; [ assumption | omega ].
-  generalize H3.
-  pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *;
-    apply Zabs_ind; intros; omega.
+  { assert (Zabs a <= Zabs p) as H2.
+      apply Zdivide_bounds; [ assumption | omega ].
+    revert H2.
+    pattern (Zabs a); apply Zabs_ind; pattern (Zabs p); apply Zabs_ind;
+    intros; omega. }
   intuition idtac.
   (* -p < a < -1 *)
-  absurd (rel_prime (- a) p); intuition.
-  inversion H3.
-  assert (- a | - a); auto with zarith.
-  assert (- a | p); auto with zarith.
-  generalize (H8 (- a) H9 H10); intuition idtac.
-  generalize (Zdivide_1 (- a) H11); intuition.
+  - absurd (rel_prime (- a) p); intuition.
+    inversion H2.
+    assert (- a | - a) by auto with zarith.
+    assert (- a | p) by auto with zarith.
+    apply H7, Zdivide_1 in H8; intuition.
   (* a = 0 *)
-  inversion H2. subst a; omega.
+  - inversion H1. subst a; omega.
   (* 1 < a < p *)
-  absurd (rel_prime a p); intuition.
-  inversion H3.
-  assert (a | a); auto with zarith.
-  assert (a | p); auto with zarith.
-  generalize (H8 a H9 H10); intuition idtac.
-  generalize (Zdivide_1 a H11); intuition.
+  - absurd (rel_prime a p); intuition.
+    inversion H2.
+    assert (a | a) by auto with zarith.
+    assert (a | p) by auto with zarith.
+    apply H7, Zdivide_1 in H8; intuition.
 Qed.
 
 (** A prime number is relatively prime with any number it does not divide *)
@@ -606,11 +605,10 @@ Qed.
 Lemma prime_rel_prime :
   forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.
 Proof.
-  simple induction 1; intros.
-  constructor; intuition.
-  elim (prime_divisors p H x H3); intuition; subst; auto with zarith.
-  absurd (p | a); auto with zarith.
-  absurd (p | a); intuition.
+  intros; constructor; intros; auto with zarith.
+  apply prime_divisors in H1; intuition; subst; auto with zarith.
+  - absurd (p | a); auto with zarith.
+  - absurd (p | a); intuition.
 Qed.
 
 Hint Resolve prime_rel_prime: zarith.
@@ -635,7 +633,7 @@ Lemma prime_mult :
   forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b).
 Proof.
   intro p; simple induction 1; intros.
-  case (Zdivide_dec p a); intuition.
+  case (Zdivide_dec p a); nintuition.
   right; apply Gauss with a; auto with zarith.
 Qed.