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, 10 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 91501ebcd9..cc365dce9f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -41,6 +41,16 @@ Tactics
   "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
 - New command "r string" that interprets "idtac string" as a breakpoint
   and jumps to its next use in Ltac debugger.
+- Tactic "tauto" was exceptionally able to destruct other connectives
+  than the binary connectives "and", "or", "prod", "sum", "iff".  This
+  non-uniform behavior has been fixed (bug #2680) and tauto is
+  slightly weaker. On the opposite side, new tactic "dtauto" is able
+  to destruct any record-like inductive types, superseding the old
+  version of "tauto".
+- Similarly, "intuition" has been made more uniform and, where it now
+  fails, "dintuition" can be used. Moreover, both of them are now only
+  lazily unfolding the occurrences of "not" in goal. Some extra
+  "unfold not in *" might have to be added for compatibility.
 
 Libraries