4

所以，我有一个看起来像这样的证明：

induction t; intros; inversion H ; crush.

它解决了我的所有目标，但是当我这样做时Qed，我收到以下错误：

Cannot guess decreasing argument of fix.

所以在生成的证明项的某个地方，存在没有充分根据的递归。问题是，我不知道在哪里。

有没有办法调试这种错误，或者查看策略脚本生成的（可能是非停止的）证明项？

4

3 回答 3

6

您可以使用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.
于 2018-02-20T02:15:40.270 回答
3

您可以Show Proof.在证明模式中使用命令打印到目前为止生成的证明项。

于 2018-02-20T00:01:08.967 回答
3

除了其他出色的答案之外，我还想指出，induction在交互模式Fixpoint中使用通常是一个错误，因为您要递归两次。在交互模式下编写固定点通常很棘手，因为大多数自动化工具会在每一个可能的机会中愉快地进行递归调用，即使它没有根据。

我建议在证明脚本中使用Definition而不是Fixpoint使用。induction这会调用显式递归器，从而可以更好地控制自动化。缺点是灵活性降低，因为固定点的限制比递归器少——但正如我们所见，这既是福也是祸。

于 2018-07-28T05:22:15.177 回答