From e1f5180e88bf02a22c954ddbdcbdfeb168d264a6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 15 Apr 2012 22:06:11 +0000 Subject: 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 --- theories/Structures/OrderedType.v | 4 ++-- theories/Structures/OrdersLists.v | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index f84cdf32c..beb10a833 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -223,7 +223,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. Proof. exact (InfA_ltA lt_strorder). Qed. Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. +Proof. exact (InfA_eqA eq_equiv lt_compat). Qed. Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. @@ -396,7 +396,7 @@ Module KeyOrderedType(O:OrderedType). Qed. Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. - Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed. + Proof. exact (InfA_eqA eqk_equiv ltk_compat). Qed. Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index f83b63779..059992f5b 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -32,7 +32,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. Proof. exact (InfA_ltA lt_strorder). Qed. Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. +Proof. exact (InfA_eqA eq_equiv lt_compat). Qed. Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. -- cgit v1.2.3