在 Coq 中,有没有办法查看 tauto 应用的策略?

如何解决在 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 证明的目标 - 否则证明项将难以消化。

版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。

相关推荐


Selenium Web驱动程序和Java。元素在(x,y)点处不可单击。其他元素将获得点击?
Python-如何使用点“。” 访问字典成员?
Java 字符串是不可变的。到底是什么意思?
Java中的“ final”关键字如何工作?(我仍然可以修改对象。)
“loop:”在Java代码中。这是什么,为什么要编译?
java.lang.ClassNotFoundException:sun.jdbc.odbc.JdbcOdbcDriver发生异常。为什么?
这是用Java进行XML解析的最佳库。
Java的PriorityQueue的内置迭代器不会以任何特定顺序遍历数据结构。为什么?
如何在Java中聆听按键时移动图像。
Java“Program to an interface”。这是什么意思?
Java在半透明框架/面板/组件上重新绘画。
Java“ Class.forName()”和“ Class.forName()。newInstance()”之间有什么区别?
在此环境中不提供编译器。也许是在JRE而不是JDK上运行?
Java用相同的方法在一个类中实现两个接口。哪种接口方法被覆盖?
Java 什么是Runtime.getRuntime()。totalMemory()和freeMemory()?
java.library.path中的java.lang.UnsatisfiedLinkError否*****。dll
JavaFX“位置是必需的。” 即使在同一包装中
Java 导入两个具有相同名称的类。怎么处理?
Java 是否应该在HttpServletResponse.getOutputStream()/。getWriter()上调用.close()?
Java RegEx元字符(。)和普通点?