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: Aug 15 2022 at 02:13 UTC