coq - 在Coq中，有没有办法看到tauto应用的策略？

Question

有没有办法看到tauto所应用的策略？即，运行 tauto 并获取要应用的策略列表(不包括 tauto)？

Answer 1

tauto 是直接用 OCaml 编写的策略，因此它不应用其他策略 - 它构造一个证明项。但你可以看看它构造的证明项。

例如

Goal forall P Q : Prop, P /\ Q -> P.
tauto.
Show Proof.

结果:

(fun (P Q : Prop) (H : P /\ Q) => and_ind (fun (H0 : P) (_ : Q) => H0) H)

fun (P Q : Prop) (H : P/\Q) 对应于 intros P Q H。然后它使用 and_ind 并以函数作为参数。这对应于exact (and_ind (fun P' Q' => P') H)。。正如您所看到的，技巧在于 and_ind 的函数参数的构造。

查看这些证明术语很有启发性，但如果您手动进行证明，通常会采用与 tauto 不同的方式。

如果您查看 tauto 的证明术语，请隔离您用 tauto 证明的目标 - 否则证明术语将难以理解。