给定a和b之间的关系，从(b --> c)证明(a --> c)
给定a和b之间的关系，从(b --> c)证明(a --> c)
提问于 2018-08-29 16:42:41
下面是我试图证明的一个具体的玩具示例：
theory Prop imports Main
begin
lemma
fixes func1 :: "'a => 'a"
and func2 :: "'a => 'a"
and func3 :: "'a => 'a"
assumes "∀ x y. func1 x = func1 y --> func3 x = func3 y"
and "∀ x. func1 x = func2 x"
shows "∀ x y. func2 x = func2 y --> func3 x = func3 y"
proof -
from assms show ?thesis by auto
qed
end验证没有成功，Isabelle 2018继续运行，"by auto“部分显示为紫色。我该如何证明这类引理呢？
回答 1
Stack Overflow用户
回答已采纳
发布于 2018-08-30 03:32:13
似乎您的问题导致了simplifier (这是auto的一部分)循环。我真的不明白为什么，但这些事情确实偶尔会发生。
发生这种情况时，有时运行try0 (它只尝试几个常见的自动证明方法并返回那些成功的方法)或sledgehammer (它试图将问题转换为更简单的形式并将其提供给外部证明者；如果他们可以证明它，然后尝试将证明转换回Isabelle)会有所帮助。
在这种情况下，try0和sledgehammer都发现一个简单的apply metis就可以完成这项工作。像auto和simp这样的方法做了很多事情，包括，最值得注意的是，使用一组预定义的规则进行“愚蠢的”重写。metis在它所做的事情上更聪明一些，但你需要手动给出它应该使用的每一个事实，而且它不太适合Isabelle/HOL。
然而，由于这个问题是简单的一阶逻辑，metis可以在没有明确给定事实的情况下很容易地自己解决它们，并且它设法避免导致auto和simp发散的任何陷阱。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/52073140
复制相关文章
相似问题