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.