Don’t `?` and `|` perform backtracking? · General

I thought that the proof method combinators ? and | 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.

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 ? and |, the 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)

First, destruction_rule becomes 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 ? and | 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?

Stream: General

Topic: Don’t `?` and `|` perform backtracking?

Wolfgang Jeltsch (Nov 23 2021 at 20:54):