## Stream: General

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

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

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.

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 `?` 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?

Last updated: Dec 07 2023 at 08:19 UTC