I thought that the proof method combinators
| perform backtracking, but from some experiments I conclude that they perform what I know as “fast-back”: different alternatives are tried, but as soon as a working one has been chosen this choice isn’t revised if a later method fails.
Let me illustrate this with some examples.
Consider the following attempt to prove a trivial lemma:
lemma fixes n m :: nat shows "n < m ⟹ n < m" by ((drule Suc_mono)?, assumption)
Apparently, the premise is the conclusion, so that
assumption could solve the goal. However, we first apply
drule Suc_mono, which turns the premise into
Suc n < Suc m, thus making it unusable. As a result,
assumption fails. If
? would perform backtracking, it would now consider the other alternative of
(drule Suc_mono)?: just doing nothing. However, it apparently doesn’t do that, as the above proof fails. It seems that the “do nothing” alternative would have only been chosen if
drule Suc_mono would have failed.
The situation seems to be analogous for
|. Consider the following variant of the above code:
lemma fixes n m :: nat shows "n < m ⟹ n < m" by ((drule Suc_mono | insert TrueI), assumption)
Here, the alternative is not doing nothing, but inserting
True as an extra premise, which wouldn’t impair the
assumption method in solving the goal. Still, this proof fails, apparently because, after the successful execution of
drule Suc_mono, the choice for the first alternative is not questioned even when
assumption fails because of this choice.
In contrast to
match method does perform backtracking. Consider the following variant of the above code examples:
lemma fixes n m :: nat shows "n < m ⟹ n < m" by (match Suc_mono TrueE [OF TrueI] in destruction_rule: _ ⇒ ‹drule destruction_rule›, assumption)
Suc_mono, which causes the subsequent
assumption to fail, as above. However,
match performs backtracking because of this failure of a subsequent proof method, causing
destruction_rule to become
TrueE [OF TrueI], which is
?P ⟹ ?P. Applying
drule with this fact leaves the premise alone, and subsequently
assumption solves the goal.
Did I get this correctly that
| only perform “fast-back”, meaning they only revise their decisions when the argument method (in the case of
?) or the first argument method (in the case of
|) fails, or is there something else going on here?
Last updated: Dec 07 2023 at 08:19 UTC