下面是我试图证明的一个具体的玩具示例:
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“部分显示为紫色。我该如何证明这类引理呢?
发布于 2018-08-30 03:32:13
似乎您的问题导致了simplifier (这是auto
的一部分)循环。我真的不明白为什么,但这些事情确实偶尔会发生。
发生这种情况时,有时运行try0
(它只尝试几个常见的自动证明方法并返回那些成功的方法)或sledgehammer
(它试图将问题转换为更简单的形式并将其提供给外部证明者;如果他们可以证明它,然后尝试将证明转换回Isabelle)会有所帮助。
在这种情况下,try0
和sledgehammer
都发现一个简单的apply metis
就可以完成这项工作。像auto
和simp
这样的方法做了很多事情,包括,最值得注意的是,使用一组预定义的规则进行“愚蠢的”重写。metis
在它所做的事情上更聪明一些,但你需要手动给出它应该使用的每一个事实,而且它不太适合Isabelle/HOL。
然而,由于这个问题是简单的一阶逻辑,metis
可以在没有明确给定事实的情况下很容易地自己解决它们,并且它设法避免导致auto和simp发散的任何陷阱。
https://stackoverflow.com/questions/52073140
复制相似问题