Может ли сочинение попробовать и повторить привести к бесконечному циклу в Coq?

Question

Я знаю, что повторение применяется тактически несколько раз, пока не сработает.

Повторная тактика принимает другую тактику и продолжает применять эту тактику, пока не потерпит неудачу.

и тактика попытки ничего не делает, когда она "терпит неудачу":

Если T - это тактика, то попробуйте T - это такая же тактика, как и T, за исключением того, что, если T терпит неудачу, попытка T вообще ничего не делает (вместо неудачи).

Означает ли это, если бы я сделал что-то вроде:

repeat (try reflexivity).

если рефлексивность не срабатывает, то попытка ничего не делает (но не дает сбой), поэтому повторение просто продолжает применяться try reflexivity, Это правильно? Или что происходит?

---

Я спрашиваю, потому что увидел эту теорему:

Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (try (left; reflexivity); right).
Qed.

когда я задал связанный вопрос: являются ли тактика Coq правой ассоциативной или левой ассоциативной?

источник: https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html

Answer 1

Фактическая семантика repeat в том, что он останавливается, если тактика не дает прогресса.

https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html?highlight=repeat

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

Тем не менее, это действительно возможно сделать repeat идти в бесконечном цикле, пока он делает успехи на каждой итерации. Например, следующий скрипт пытается создать список, всегда используя cons конструктор, а не заканчивая в какой-то момент nil:

Theorem there_exists_a_list_of_nat : list nat.
Proof.
  repeat right.

Это действительно будет цикл навсегда (убедитесь, что вы знаете, как отменить вычисление, прежде чем пытаться запустить его).

Answer 2

Этот шаблон не приводит к бесконечному циклу, потому что повторение t останавливается, когда t не может прогрессировать, а не когда происходит сбой. Документация ( https://coq.inria.fr/refman/proof-engine/ltac.html) добавляет это в следующем предложении, хотя, безусловно, может быть более понятным.

Дополнительное объяснение в Фондах программного обеспечения неверно; он утверждает, что повтор входит в бесконечный цикл, когда ему дается тактика, которая всегда успешна, и дает в качестве примера повторение упрощенного, но повторяет упрощенные работы (после не более одного раунда упрощения он ничего не сделает, если запустить снова, поэтому повторение останавливается).