diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-15 22:06:11 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-15 22:06:11 +0000 |
commit | e1f5180e88bf02a22c954ddbdcbdfeb168d264a6 (patch) | |
tree | 86e1f5b98681f5e85aef645a9de894508d98920b /theories/FSets | |
parent | 25c1cfeea010b7267955d6683a381b50e2f52f71 (diff) |
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
Diffstat (limited to 'theories/FSets')
-rw-r--r-- | theories/FSets/FMapFacts.v | 14 | ||||
-rw-r--r-- | theories/FSets/FSetProperties.v | 2 |
2 files changed, 4 insertions, 12 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 0c1448c9b..9fef1dc63 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -519,7 +519,7 @@ Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, elements_mapsto_iff. unfold eqb. -rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto. +rewrite <- findA_NoDupA; dintuition; try apply elements_3w; eauto. Qed. Lemma elements_b : forall m x, @@ -679,8 +679,8 @@ Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m. Proof. unfold Empty; intros m m' Hm; intuition. -rewrite <-Hm in H0; eauto. -rewrite Hm in H0; eauto. +rewrite <-Hm in H0; eapply H, H0. +rewrite Hm in H0; eapply H, H0. Qed. Add Parametric Morphism elt : (@is_empty elt) @@ -1872,13 +1872,7 @@ Module OrdProperties (M:S). add_mapsto_iff by (auto with *). unfold O.eqke, O.ltk; simpl. destruct (E.compare t0 x); intuition. - right; split; auto; ME.order. - ME.order. - elim H. - exists e0; apply MapsTo_1 with t0; auto. - right; right; split; auto; ME.order. - ME.order. - right; split; auto; ME.order. + elim H; exists e0; apply MapsTo_1 with t0; auto. Qed. Lemma elements_Add_Above : forall m m' x e, diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 1bad80615..eec7196b7 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -995,8 +995,6 @@ Module OrdProperties (M:S). leb_1, gtb_1, (H0 a) by auto with *. intuition. destruct (E.compare a x); intuition. - right; right; split; auto with *. - ME.order. Qed. Definition Above x s := forall y, In y s -> E.lt y x. |