Coq: просмотр контрольного термина во время написания контрольного сценария
Итак, у меня есть доказательство, которое выглядит так:
induction t; intros; inversion H ; crush.
Это решает все мои цели, но когда я делаю QedЯ получаю следующую ошибку:
Cannot guess decreasing argument of fix.
Так что где-то в сгенерированном термине доказательства есть необоснованная рекурсия. Проблема в том, что я понятия не имею, где.
Есть ли способ отладить такого рода ошибки или увидеть (возможно, не прерывающий) термин доказательства, который генерирует сценарий тактики?
3 ответа
Ты можешь использовать Show Proof. чтобы просмотреть срок доказательства до сих пор.
Другая команда, которая может помочь увидеть, где рекурсия пошла не так, Guarded., который запускает проверку завершения на срок доказательства до сих пор. Вам нужно будет разбить тактический сценарий на независимые предложения, чтобы использовать его. Вот пример:
Fixpoint f (n:nat) : nat.
Proof.
apply plus.
exact (f n).
Guarded.
(* fails with:
Error:
Recursive definition of f is ill-formed.
...
*)
Defined.
Вы можете использовать Show Proof. команда в режиме доказательства, чтобы напечатать полученный до сих пор термин доказательства.
В дополнение к другим отличным ответам, я также хочу отметить, что использование induction внутри интерактивного режима Fixpoint обычно это ошибка, потому что вы повторяетесь дважды. Написание точек фиксации в интерактивном режиме часто бывает сложно, потому что большинство инструментов автоматизации с радостью будут делать рекурсивный вызов при каждой возможной возможности, даже если она будет необоснованной.
Я бы посоветовал использовать Definition вместо Fixpoint и использовать induction в сценарии доказательства. Это вызывает явный рекурсор, который позволяет намного лучше контролировать автоматизацию. Недостатком является снижение гибкости, поскольку у фиксированных точек меньше ограничений, чем у рекурсоров, но, как мы видели, это одновременно и благословение, и проклятие.