isabelle - 在 Isabelle 中证明自然的递归“小于”定义的基本性质
问题描述
为了学习目的,我试图重新创建自然数的简化版本(因为它涉及归纳定义、递归函数等......)。然而,在那个过程中,我陷入了一些我认为非常微不足道的事情。
基本上,我有一个自然数的natt
定义 ' ' 和一个 ' <
' 关系的定义:
datatype natt = Zero | Succ natt
primrec natt_less :: "natt ⇒ natt ⇒ bool" (infixl "<" 75) where
"natt_less n Zero = False"
| "natt_less n (Succ m') = (case n of Zero ⇒ True | Succ n' ⇒ natt_less n' m')"
从这些,我试图证明<
关系的 3 个基本属性:
- 非反身性:
~ (a < a)
- 非对称:
a < b ⟹ ~ (b < a)
- 传递性:
a < b ⟹ b < c ⟹ a < c
我能够证明第一个,但不能证明其他。更让我吃惊的是,有一些子引理可以帮助解决这些问题,例如Succ a < b ⟹ a < b
或a < b ⟹ a < Succ b
,这似乎更加微不足道,但即使经过多次尝试a < b ∨ a = b ∨ b < a
,我也无法证明。似乎只有其中一个(包括and )足以证明其余部分,但我无法证明其中任何一个。2.
3.
我主要是尝试使用归纳法。加上我自己做出定义的事实,有两种可能性 - 我的定义是错误的,并且没有所需的属性,或者我缺少一些方法/参数。所以,我有两个问题:
- 我的定义是否错误(即它不能准确表示
<
并且缺少所需的属性)?如果是这样,我该如何解决? - 如果不是,我如何证明这些看似微不足道的性质?
就上下文而言,我目前的尝试是通过归纳,我可以证明基本情况,但总是陷入归纳情况,不知道在哪里进行假设,例如在这个例子中:
lemma less_Succ_1: "Succ a < b ⟹ a < b"
proof (induction b)
case Zero
assume "Succ a < Zero"
then have "False" by simp
then show ?case by simp
next
case (Succ b)
assume "(Succ a < b ⟹ a < b)" "Succ a < Succ b"
then show "a < Succ b" oops
解决方案
经过user9716869的一些提示后,很明显我的主要问题是arbitrary
对induction
. 使用(induction _ arbitrary: _)
and (cases _)
(详见参考手册),证明非常简单。
由于这些是为教育目的而制作的,因此以下证明并非旨在简洁,而是要使每一步都非常清楚。如果需要更多的自动化,其中大部分可以大大减少,有些可以在一行中完成(我在引理下方留下了评论)。
注意:在这些证明中,我们使用了一个关于归纳类型的隐式引理,它们的内射性(这意味着(Succ a = Succ b) ≡ (a = b)
和Zero ≠ Succ a
)。此外,(Succ a < Succ b) ≡ (a < b)
根据定义。
首先,我们证明 2 个有用的引理:
a < b ⟹ b ≠ Zero
b ≠ Zero ⟷ (∃ b'. b = Succ b')
lemma greater_not_Zero [simp]: "a < b ⟹ b ≠ Zero"
(*by clarsimp*)
proof
assume "a < b" "b = Zero"
then have "a < Zero" by simp
then show "False" by simp
qed
lemma not_Zero_is_Succ: "b ≠ Zero ⟷ (∃ b'. b = Succ b')"
(*by (standard, cases b) auto*)
proof
show "b ≠ Zero ⟹ ∃ b'. b = Succ b'"
proof (cases b)
case Zero
assume ‹b ≠ Zero›
moreover note ‹b = Zero›
ultimately show "∃b'. b = Succ b'" by contradiction
next
case (Succ b')
assume ‹b ≠ Zero›
note ‹b = Succ b'›
then show "∃b'. b = Succ b'" by simp
qed
next
assume "∃ b'. b = Succ b'"
then obtain b'::natt where "b = Succ b'" by clarsimp
then show "b ≠ Zero" by simp
qed
有了这些,我们可以证明 3 个主要陈述:
- 非反身性:
~ (a < a)
- 非对称:
a < b ⟹ ~ (b < a)
- 传递性:
a < b ⟹ b < c ⟹ a < c
lemma less_not_refl [simp]: "¬ a < a"
(*by (induction a) auto*)
proof (induction a)
case Zero
show "¬ Zero < Zero" by simp
next
case (Succ a)
note IH = ‹¬ a < a›
show "¬ Succ a < Succ a"
proof
assume "Succ a < Succ a"
then have "a < a" by simp
then show "False" using IH by contradiction
qed
qed
lemma less_not_sym: "a < b ⟹ ¬ b < a"
proof (induction a arbitrary: b)
case Zero
then show "¬ b < Zero" by simp
next
case (Succ a)
note IH = ‹⋀b. a < b ⟹ ¬ b < a›
and IH_prems = ‹Succ a < b›
show "¬ b < Succ a"
proof
assume asm:"b < Succ a"
have "b ≠ Zero" using IH_prems by simp
then obtain b'::natt where eq: "b = Succ (b')"
using not_Zero_is_Succ by clarsimp
then have "b' < a" using asm by simp
then have "¬ a < b'" using IH by clarsimp
moreover have "a < b'" using IH_prems eq by simp
ultimately show "False" by contradiction
qed
qed
lemma less_trans [trans]: "a < b ⟹ b < c ⟹ a < c"
proof (induction c arbitrary: a b)
case Zero
note ‹b < Zero›
then have "False" by simp
then show ?case by simp
next
case (Succ c)
note IH = ‹⋀a b. a < b ⟹ b < c ⟹ a < c›
and IH_prems = ‹a < b› ‹b < Succ c›
show "a < Succ c"
proof (cases a)
case Zero
note ‹a = Zero›
then show "a < Succ c" by simp
next
case (Succ a')
note cs_prem = ‹a = Succ a'›
have "b ≠ Zero" using IH_prems by simp
then obtain b' where b_eq: "b = Succ b'"
using not_Zero_is_Succ by clarsimp
then have "a' < b'" using IH_prems cs_prem b_eq by simp
moreover have "b' < c" using IH_prems b_eq by simp
ultimately have "a' < c" using IH by simp
then show "a < Succ c" using cs_prem by simp
qed
qed
推荐阅读
- javascript - 顺利移动谷歌地图标记
- python-3.x - 将 IntVar() 值转换为 Int
- azure - 无法从 Azure REST API 获取指标
- arrays - 删除后 UI 重新呈现并获取所有复选框
- node.js - 这个异步转换的承诺是否正确,为什么不需要等待?
- jenkins-pipeline - 仅当分支与 Jenkinsfile 管道中的主节点匹配时如何询问用户输入?
- python - 在 QWebEngineView 中获取 sslerrors 信号
- javascript - 使用 JavaScript 方向 API,需要在步行和公交中混合方向指令
- html - CSS将图像与文本对齐
- javascript - 在两个分隔符上拆分字符串?