代码之家 › 专栏 › 技术社区 › jmite

Coq:在校样脚本编写期间查看校样术语

ltac theorem-proving termination dependent-type coq

4

jmite · 技术社区 · 6 年前

所以,我有一个这样的证明:

induction t; intros; inversion H ; crush.

它解决了我所有的目标 Qed ,我得到以下错误:

Cannot guess decreasing argument of fix.

所以在生成的证明项中的某个地方,有一个非良好的递归。问题是,我不知道在哪里。

有没有办法调试这种错误,或者查看战术脚本生成的(可能是不间断的)证明项?

3 回复 | 直到 6 年前

1

6

Tej Chajed 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.

2

3

Arthur Azevedo De Amorim 6 年前

您可以使用 Show Proof. 命令inside-proof mode打印到目前为止生成的校对项。

3

lily 6 年前

除了其他优秀的答案之外,我还想指出 induction 在交互模式内 Fixpoint 通常是一个错误,因为您重复了两次。在交互模式下编写固定点通常很棘手,因为大多数自动化工具都会很乐意在任何可能的机会进行递归调用,即使这样做是没有根据的。

我建议使用 Definition 而不是 固定点 和使用 就职 在校对脚本中。这将调用显式递归器,从而可以更好地控制自动化。缺点是灵活性降低,因为不动点的限制比递归少——但正如我们所看到的,这既是福也是祸。