Может ли попытка повторения привести к бесконечному циклу в 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#coq:tacn.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#coq:tacn.repeat) добавляет это в следующем предложении, хотя это, безусловно, может быть более ясным.

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