isabelle - 这个伊莎贝尔证明有什么问题?
问题描述
该模式生成器在给定位置生成具有给定数字的列表,所有其他值为零。
fun pattern_one_value :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat list" where
"pattern_one_value _ _ _ 0 = []" |
"pattern_one_value pos pos1 val lng =
(if pos = pos1 then val else 0) # (pattern_one_value pos (pos1 + 1) val (lng - 1))"
以下引理旨在证明生成的列表在给定位置包含正确的值。
lemma pattern_one_value_check [simp]: "∀pos val. pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
proof(induct lng)
case 0 then show ?case by simp
next
case (Suc lng) then show ?case by auto
qed
这似乎是一个正确的证明;然而,val
将生成函数的 cons 表达式更改为任意数,例如(if pos = pos1 then 7 else 0) # ...
,证明仍然成立,因为基础假设和归纳假设都是错误的。我哪里错了?谢谢你的帮助。
解决方案
这似乎是一个正确的证明;但是,将生成函数的 cons 表达式中的 val 更改为任意数,例如
(if pos = pos1 then 7 else 0) # ...
,证明仍然成立,因为基础假设和归纳假设都是错误的。我哪里错了?
我相信这个问题与试图将 HOL 的通用量词∀
视为等同于 Pure 的通用量词有关⋀
。pattern_one_value_check
实际上,如您的问题所述,可以从定理的前提证明任何事情。的确:
lemma pattern_one_value_check'[simp]:
"(∀pos val::nat. pos < (lng::nat)) = False"
by auto
lemma pattern_one_value_check''[simp]:
"(∀pos val::nat. pos < (lng::nat)) ⟹ P"
by auto
我相信你的意思是Pure
在定理的陈述中使用 ' 的普遍量化,例如
lemma pattern_one_value_check [simp]:
"⋀pos val. pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
proof(induct lng)
case 0 then show ?case by simp
next
case (Suc lng) then show ?case sorry
qed
事实上,即使这样也没有必要。以下定理一旦被证明,将在上下文中与上述定理相同:
lemma pattern_one_value_check' [simp]:
"pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
proof(induct lng)
case 0 then show ?case by simp
next
case (Suc lng) then show ?case sorry
qed
如果您寻求更详细的解释,请参阅 Isar-ref 中的第 2.1 节和文档“Isabelle/HOL 中的编程和证明”,两者都是官方文档的一部分。
作为旁注,我不得不提一下,也许有一种更简单的方法来定义pattern_one_value
. 在这种情况下, 的证明pattern_one_value_check
似乎也更容易:
definition pattern_one_value :: "nat ⇒ nat ⇒ nat ⇒ nat list"
where "pattern_one_value val pos len = list_update (replicate len 0) pos val"
lemma pattern_one_value_check:
assumes "pos < len"
shows "pattern_one_value val pos len ! pos = val"
using assms unfolding pattern_one_value_def
apply(induct len)
subgoal by auto
subgoal by (metis length_replicate nth_list_update)
done
推荐阅读
- r - 从R中的字符串中获取下两个单词
- beautifulsoup - BeautifulSoup original_encoding 不返回
- c++ - 如何停止从字符串中读取换行符?
- microsoft-edge - Edge addon can not capture audio on some Windows version
- google-colaboratory - 如何使用 pip 在 Google Colab 实例上安装 Talib 模块
- java - 从知道 uid 的 firebase 检索用户名
- mongodb - 计算mongodb中对象的不同值
- mysql - 如何使用 mysql 从图像表中获取总计数?
- android - 无法运行 react-native 应用程序
- python - 为什么我不能遍历 python 中的列表