coq - Coq:在校对脚本编写过程中查看校对术语

Question

因此，我有一个看起来像这样的证明:

induction t; intros; inversion H ; crush.

它解决了我所有的目标，但是当我执行 Qed时，出现以下错误:
Cannot guess decreasing argument of fix.
因此，在生成的证明词中的某个地方，存在没有充分根据的递归。问题是，我不知道在哪里。

有没有一种方法可以调试这种错误，或者查看战术脚本生成的(可能不会停止)证明术语？

Answer 1

到目前为止，您可以使用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.