会员证明

问题描述 投票:2回答:1

我需要证明以下内容:

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

此时的子目标太长了,我不知道如何继续。

我不是在寻找一个完整的答案,只是提示如何处理这个引理。而且,对于刚刚学习伊莎贝尔的人来说,这个证明是一个简单的证明还是非常困难的证明?

isabelle proof
1个回答
1
投票

掠夺者:可以使用标准列表归纳法和auto来证明该定理,即类似于by (induct xs ...) (auto simp: ...)的定理。我故意在证明中省略了你自己填写的部分。您需要考虑是否需要将任何变量(即mx)指定为arbitrary,并且还要了解简化器可能需要哪些信息(在min_list理论中查找List规范中的线索)。

关于你对这个问题的难度的问题,我认为,困难是经验的一个功能。当然,当我开始学习Isabelle时,我发现很难形成类似于你问题中的证明的证明。在Isabelle编程一段时间之后(在回答这个问题时,我必须在Isabelle中累积相当于4-5个月的全职编码),这些问题似乎不再对我构成重大挑战。当然,还有其他因素需要考虑,例如以前的数学或逻辑培训和以前的编码经验。


来自正在学习Isabelle的人的一般建议(该建议可能与专业教师通常建议的方法不一致)

我相信,在证明类似的结果时,重要的是要理解Isabelle主要是用于“纸笔”证明形式化的工具。因此,在试图将其正式化之前,手头上的“纸笔”证明非常重要。在攻击类似问题时我会建议以下一般方法:

  1. 在纸上写下证明。
  2. 使用Isar将证明形式化,提供尽可能多的细节,而不是过多关注证明的长度。另外,尽量不要依赖自动推理工具(即autoblastmesonmetisfastforce),并尽可能多地使用ruleintro等直接方法。
  3. 一旦您的Isar证明完成,将自动推理工具(例如autoblast)应用于您的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是隐式定义的,并构成datatypelist基础结构的一部分(参见文档“在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)axxs。修复axxs。假设m = min_list (a # x # xs)。然后它仍然显示m ∈ set (a # x # xs)。鉴于m = min_list (a # x # xs),从min_list的定义,很容易推断m = am = min_list (x # xs)。明确考虑这些情况:

  • 案例一:m = aa ∈ 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证明。此外,请注意,证明可能不太理想 - 我可能会在以后编辑证明。

© www.soinside.com 2019 - 2024. All rights reserved.