如何解决在 Coq 中,有没有办法查看 tauto 应用的策略?
有没有办法查看tauto应用的战术?即,运行 tauto 并获取要应用的策略列表(不包括 tauto)?
解决方法
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 证明的目标 - 否则证明项将难以消化。