Info vernacular命令如何工作？其数值参数与输出含义是什么

1. Info vernacular 命令的工作机制 #

Info 是 Coq 内置的调试类 vernacular 命令，用于将用户输入的高层战术（tactic）展开为 Coq 内核实际执行的低层级操作，输出展开过程的同时不会修改当前的证明状态。
它的核心逻辑是拦截战术的执行流程，按照用户指定的详细程度，把战术内部的调用链、最终转化的内核指令打印出来，方便用户理解高层战术的底层实现、排查战术执行不符合预期的问题。

2. 传入自然数参数的原因 #

这个自然数是详细程度阈值，取值范围为 1 到 100：

• 数值越小，输出越精简，仅展示最上层的展开结果，会省略嵌套的子战术调用、内部参数绑定等细节
• 数值越大，输出越完整，当你传入 100（最高阈值）时，Info 会无省略打印战术所有的底层展开步骤，包括最深层级的内核调用、隐式参数绑定等内容
  比如如果你执行 Info 1 split，输出会简化为类似 refine (conj _ _) 的形式，不会展示更底层的参数绑定信息。

3. 示例输出的具体含义 #

你的示例中，执行 Info 100 split 时的证明上下文为：

• 目标：P /\ Q
• 上下文变量：P : Prop、Q : Prop、HP : P、HQ : Q
  输出内容 simple refine ?X10@{__:=P; __:=Q; __:=HP; __:=HQ} 的各部分含义如下：
• simple refine：Coq 内核的底层构造战术，作用是用传入的项填充当前证明目标，支持保留未填充的洞（元变量）后续继续构造
• ?X10：Coq 自动生成的元变量，对应当前待构造的 P /\ Q 类型的证明项，X 后的数字是 Coq 为元变量分配的内部唯一标识
• @{__:=P; __:=Q; __:=HP; __:=HQ}：元变量的隐式参数实例化列表，表示这个元变量依赖的所有隐式参数，已经被当前上下文里的 P、Q、HP、HQ 四个变量完成实例化，不需要用户额外手动提供
  这个输出本质是说明，你调用的 split 战术在当前合取目标的场景下，底层最终转化为了上述带参数绑定的 simple refine 调用完成目标拆分。

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