Coq：编写证明脚本时查看证明项及递归错误调试咨询

遇到这种Cannot guess decreasing argument of fix的错误真的很闹心——明明战术脚本跑完所有目标了，结果临门一脚Qed报错，十有八九是证明项里藏了Coq没法自动验证终止性的递归结构。下面分享几个我常用的调试和排查方法：

1. 先把生成的证明项揪出来看 #

要定位问题，首先得知道战术到底生成了什么样的证明项。可以用这些命令：

• 用Show Proof.：在你原本要写Qed.的位置先加这个命令，Coq会打印当前的证明项草稿。如果输出太长，先执行Set Printing Depth 100.（数字可以调整）来控制显示深度，避免输出爆炸。
• 开启Set Printing All.：这个选项会让Show Proof显示更多细节，包括隐含的类型转换、自动生成的fixpoint等，方便你找到那些可疑的递归定义。
• 导出到文件慢慢看：如果证明项实在太长，用Dump Proof "my_proof_term.v".把它导出到文件里，直接搜索关键词fix，找到那些Coq没法确定递减参数的递归部分。

2. 逐步拆解战术脚本排查根源 #

有时候问题出在某个自动战术（比如auto、eauto）或者induction的误用，偷偷生成了非良基递归。可以试试：

• 分段执行脚本：把你的战术脚本拆成小段，每执行几个战术就跑一次Show Proof.，对比每次的证明项变化，找到引入可疑fixpoint的那个步骤。
• 替换自动战术：把auto这类“黑盒”战术换成手动的apply、rewrite，看看是不是自动战术偷偷引入了递归。
• 检查归纳假设的使用：如果用了induction，确保你在递归调用时确实用了更小的参数——有时候战术会不小心用了原参数而不是归纳假设里的递减版本，导致Coq认不出来。

3. 手动帮Coq指定递减参数 #

如果找到了问题的fixpoint，可以手动给Coq递个“提示”：

• 用fix命令手动写递归部分时，明确标注struct <arg>，比如fix f n struct n := ...，告诉Coq递归是在n这个参数上递减的。
• 对于用refine或者pose引入的递归，也可以加上{struct <arg>}的标注，比如refine (fix f n {struct n} := ...).

4. 用调试工具深挖细节 #

• 开启Set Debug "tactic".：这个选项会让Coq打印战术执行的详细过程，包括每个战术生成的证明项片段，帮你精准定位哪一步出了问题。
• 进入Ltac Debug.模式：执行这个命令后，你可以单步执行战术，每一步都能查看当前的证明状态和生成的证明项部分，像调试程序一样排查问题。

内容的提问来源于stack exchange，提问作者Joey Eremondi