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, 6 insertions, 4 deletions

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 70f4ff0d9..944e7da21 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -43,7 +43,7 @@ Hint Immediate Rge_refl: rorders.
 
 Lemma Rlt_irrefl : forall r, ~ r < r.
 Proof.
-  generalize Rlt_asym. intuition eauto.
+  intros r H; eapply Rlt_asym; eauto.
 Qed.
 Hint Resolve Rlt_irrefl: real.
 
@@ -64,7 +64,9 @@ Qed.
 (**********)
 Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2.
 Proof.
-  generalize Rlt_not_eq Rgt_not_eq. intuition eauto.
+  intuition.
+  - apply Rlt_not_eq in H1. eauto.
+  - apply Rgt_not_eq in H1. eauto.
 Qed.
 Hint Resolve Rlt_dichotomy_converse: real.
 
@@ -74,7 +76,7 @@ Hint Resolve Rlt_dichotomy_converse: real.
 Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2.
 Proof.
   intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
-    intuition eauto 3.
+    unfold not; intuition eauto 3.
 Qed.
 Hint Resolve Req_dec: real.
 
@@ -175,7 +177,7 @@ Proof. eauto using Rnot_gt_ge with rorders. Qed.
 Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
 Proof.
   generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *.
-  intuition eauto 3.
+  unfold not; intuition eauto 3.
 Qed.
 Hint Immediate Rlt_not_le: real.