From 9216cffaaa1ef137ef5bdb5b290a930cc6198850 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 21 Feb 2011 17:34:06 +0100 Subject: Imported Upstream version 0.2.pl2 --- Caveats.v | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'Caveats.v') diff --git a/Caveats.v b/Caveats.v index 8cef602..0d0d5ca 100644 --- a/Caveats.v +++ b/Caveats.v @@ -335,7 +335,8 @@ Goal a+b*c = c. *) Abort. -(** **** If the pattern is a unit: +(** **** If the pattern is a unit or can be instanciated to be equal + to a unit: The heuristic is to make the unit appear at each possible position in the term, e.g. transforming [a] into [1*a] and [a*1], but this @@ -351,23 +352,19 @@ Goal a+b+c = c. (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*) Abort. -(** **** If the pattern is a nullifiable, but not a unit: - - The heuristic is to make units appear around subterms that are -built with AC or A symbols. Note that this case is relevant only if -one uses [aacu_rewrite]. *) - -Hypothesis H : forall x y, (x+y)*x = x*x + y*x. +(** *** Another example of the former case is the following, where the hypothesis can be instanciated to be equal to [1] *) +Hypothesis H : forall x y, (x+y)*x = x*x + y *x. Goal a*a+b*a + c = c. (** Here, only one solution if we use the aac_instance tactic *) aac_instances <- H. - (** There are three solutions using aacu_instances (but, here, + (** There are 8 solutions using aacu_instances (but, here, there are infinitely many different solutions). We miss e.g. [a*a +b*a + (x*x + y*x)*c], which seems to be more peculiar. *) - aacu_instances <- H. -Abort. + aacu_instances <- H. + (** The 7 last solutions are the same as if we were matching [1] *) + aacu_instances H1. Abort. (** The behavior of the tactic is not satisfying in this case. It is still unclear how to handle properly this kind of situation : we plan -- cgit v1.2.3