diff options
author | Stephane Glondu <steph@glondu.net> | 2011-02-21 17:34:07 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2011-02-21 17:34:07 +0100 |
commit | 3b5a4caffd5f3d0021ea2716025efc068a0b8968 (patch) | |
tree | 6c60828fd5e7301d6e1df697b9eb11f374b9b059 /Caveats.v | |
parent | a99db68ef72f70cbb59746f14e526e3cd7608ea8 (diff) | |
parent | 9216cffaaa1ef137ef5bdb5b290a930cc6198850 (diff) |
Merge commit 'upstream/0.2.pl2'
Diffstat (limited to 'Caveats.v')
-rw-r--r-- | Caveats.v | 19 |
1 files changed, 8 insertions, 11 deletions
@@ -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 |