我需要证明以下内容:
lemma "m = min_list(x#xs) ⟹ m ∈ set (x#xs)"
用简单的英语,我需要证明“min_list(x#xs)”的返回值始终是(x#xs)的成员
我试过了:
apply(induct xs)
apply(auto)
我还尝试使用以下方法重用min_list的现有引理:
find_theorems min_list
此时的子目标太长了,我不知道如何继续。
我不是在寻找一个完整的答案,只是提示如何处理这个引理。而且,对于刚刚学习伊莎贝尔的人来说,这个证明是一个简单的证明还是非常困难的证明?
掠夺者:可以使用标准列表归纳法和auto
来证明该定理,即类似于by (induct xs ...) (auto simp: ...)
的定理。我故意在证明中省略了你自己填写的部分。您需要考虑是否需要将任何变量(即m
或x
)指定为arbitrary
,并且还要了解简化器可能需要哪些信息(在min_list
理论中查找List
规范中的线索)。
关于你对这个问题的难度的问题,我认为,困难是经验的一个功能。当然,当我开始学习Isabelle时,我发现很难形成类似于你问题中的证明的证明。在Isabelle
编程一段时间之后(在回答这个问题时,我必须在Isabelle
中累积相当于4-5个月的全职编码),这些问题似乎不再对我构成重大挑战。当然,还有其他因素需要考虑,例如以前的数学或逻辑培训和以前的编码经验。
来自正在学习Isabelle的人的一般建议(该建议可能与专业教师通常建议的方法不一致)
我相信,在证明类似的结果时,重要的是要理解Isabelle主要是用于“纸笔”证明形式化的工具。因此,在试图将其正式化之前,手头上的“纸笔”证明非常重要。在攻击类似问题时我会建议以下一般方法:
Isar
将证明形式化,提供尽可能多的细节,而不是过多关注证明的长度。另外,尽量不要依赖自动推理工具(即auto
,blast
,meson
,metis
,fastforce
),并尽可能多地使用rule
和intro
等直接方法。Isar
证明完成,将自动推理工具(例如auto
,blast
)应用于您的Isar证明,以尽可能简化您的证明。当然,最终,当您在学习Isabelle方面取得进步时,省略1和2会变得越来越容易。
我可以提供进一步的细节,例如完整的短证明和长Isar
版本的证明。
UPDATE
根据您在评论中的要求,我提供了一个非正式的证明。
引理。 m = min_list (x # xs) ⟹ m ∈ set (x # xs)
。
备注。为了完整起见,我还提供了min_list
的定义以及有关const set
的一些注释。 min_list
的定义可以在List
理论中找到:
fun min_list :: "'a::ord list ⇒ 'a" where
"min_list (x # xs) = (case xs of [] ⇒ x | _ ⇒ min x (min_list xs))"
const set
是隐式定义的,并构成datatype
的list
基础结构的一部分(参见文档“在Isabelle / HOL中定义(Co)数据类型和原始(Co)递归函数”,如果是Isabelle)。特别是,它被称为数据类型的“set function”。 const set
的许多基本属性可以通过检查/搜索找到,例如find_theorems list.set
。我相信定理thm list.set
代表const set
的主要属性(我冒昧地重新定义了定理中的原理图变量):
set [] = {}
set (?x # ?xs) = insert ?x (set ?xs)
证明。证据是通过列表xs
上的结构归纳。归纳原理在List
理论的开头被描述为一个未命名的引理。为了完整起见,我重申以下归纳原则:
"P [] ⟹ (⋀a list. P list ⟹ P (a # list)) ⟹ P list"
基本情况:假设xs = []
,显示所有m = min_list (x # xs) ⟹ m ∈ set (x # xs)
的x
。根据min_list
的定义,看到min_list (x # []) = x
是微不足道的。同样,set (x # []) = {x}
可以直接从const set
的属性中显示出来。代入上面的谓词,仍然显示所有m = x ⟹ m ∈ {x}
的x
。这遵循基本集理论。
诱导步骤:假设⋀x. m = min_list (x # xs) ⟹ m ∈ set (x # xs)
,显示所有m = min_list (a # x # xs) ⟹ m ∈ set (a # x # xs)
,a
和x
的xs
。修复a
,x
和xs
。假设m = min_list (a # x # xs)
。然后它仍然显示m ∈ set (a # x # xs)
。鉴于m = min_list (a # x # xs)
,从min_list
的定义,很容易推断m = a
或m = min_list (x # xs)
。明确考虑这些情况:
m = a
。 a ∈ set (a # x # xs)
遵循定义。然后,m ∈ set (a # x # xs)
通过替换。m = min_list (x # xs)
。然后,从假设⋀x. m = min_list (x # xs) ⟹ m ∈ set (x # xs)
,它遵循m ∈ set (x # xs)
。因此,m ∈ set (a # x # xs)
遵循set
的属性。在所有可能的情况下m ∈ set (a # x # xs)
,这是需要证明。
因此,证据得出结论。
最后的想法。尝试将此非正式证明转换为Isar
证明。此外,请注意,证明可能不太理想 - 我可能会在以后编辑证明。