Многократные успехи в разветвлении и возврате Coq?

Question

У меня возникли проблемы с пониманием концепции multiple successes в поведении разветвления и возврата в Coq's (8.5p1, ch9.2). Например, из документации:

Откат разветвленности

Мы можем расшириться со следующей структурой:

expr1 + expr2

тактики можно рассматривать как имеющие несколько успехов. Когда тактика выходит из строя , он просит больше успехов в предыдущей тактике. expr1 + expr2 имеет все успехи v1, за которыми следуют все успехи v2.

Что я не понимаю, почему мы должны в первую очередь добиваться нескольких успехов? Разве не один успех достаточно хорош, чтобы закончить доказательство?

также из документации, кажется, что есть менее дорогостоящие правила ветвления, которые каким-то образом «предвзятым», в том числе

first [ expr1 | ::: | exprn ] 

и

expr1 || expr2 

Зачем нам нужен более дорогостоящий вариант + и не всегда использовать последние, более эффективные тактики?

Answer 1

Проблема в том, что вы иногда пытаетесь выполнить задачу, но дальнейшие подцели могут привести к решению, которое, как вы думали, будет отклонено. Если вы накапливаете все успехи, вы можете вернуться к тому месту, где вы сделали неправильный выбор, и изучить другую ветку дерева поиска.

Вот глупый пример. скажем, я хочу, чтобы доказать эту цель:

Goal exists m, m = 1. 

Теперь, это довольно простая задача, так что я мог бы сделать это вручную, но давайте не будем. Давайте напишем тактику, которая, столкнувшись с exists, пробует все возможные натуральные числа. Если я пишу:

Ltac existNatFrom n := 
    exists n || existNatFrom (S n). 

Ltac existNat := existNatFrom O. 

тогда как только я запустить existNat, система берет на себя обязательство первого успешного выбора. В частности это означает, что, несмотря на рекурсивное определение existNatFrom, при звонке existNat я всегда получаю O и только O.

Цель не может быть решена:

Goal exists m, m = 1. 
    Fail (existNat; reflexivity). 
Abort. 

С другой стороны, если я использую (+) вместо (||), я пойду через все возможные натуральные числа (в ленивой манере, используя откаты). Так писать:

Ltac existNatFrom' n := 
    exists n + existNatFrom' (S n). 

Ltac existNat' := existNatFrom' O. 

означает, что теперь я могу доказать цель:

Goal exists m, m = 1. 
    existNat'; reflexivity. 
Qed.