Как использовать авто с повторением в пользовательской тактике?

Question

В моем развитии coq я изучаю, как создать новую тактику, адаптированную к моей проблемной области, a la Prof. Adam Chlipala.

На этой странице он описывает, как создать мощную тактику, обернув repeat вокруг match, который отвечает на различные интересные условия. Затем repeat повторяет итерации, что позволяет сделать далеко идущий вывод.

Использование repeat имеет предостережение (курсив мой):

repeat, что мы используем здесь называется тактический или тактика комбинатор. Поведение repeat t состоит в том, чтобы выполнить цикл t, работающий t во всех сгенерированных подцелях, работающих t по их сгенерированных подцелей и т. Д. Когда t терпит неудачу в любой точке этого дерева поиска, этот конкретный подзаголовок оставлен для обработки поздней тактикой. Таким образом, важно, чтобы у игрока repeat была очень хорошая тактичность.

Теперь у меня уже есть мощная тактика в использовании, auto. Он аналогичным образом объединяет цепочки шагов, на этот раз найденные из баз данных подсказок. На странице auto «s:

auto либо решает полностью задачу, либо оставляет его без изменений. auto и trivial никогда не сработает.

Boo! Я уже вложил определенные усилия в курирования auto «s намекают базы данных, но, кажется, мне запрещено нанимать их в тактике использования repeat (то есть, интересные тактики.)

Есть некоторые вариации auto, которые могут потерпеть неудачу, или в противном случае правильно использовать петли?

Например, возможно, этот вариант не работает, когда он «оставляет цель целиком».

EDIT: Включение auto в петлю не «правильный» способ сделать это в любом случае (см this), но актуальный вопрос о неисправном версии авто еще, возможно, интересно.

Answer 1

Как указано @AntonTrunov, вы всегда можете использовать тактику progress, чтобы тактика не срабатывала, если цель не изменилась. В случае auto, так как он должен решить цель или оставить его неизменным, вы можете также обернуть его в solve [ auto ], который будет иметь тот же эффект, потому что он не сработает, если auto не решит цель целиком (here is the doc for solve).