isabelle - 基本伊莎贝尔序列极限证明
问题描述
正如数百人在我之前尝试过的那样,我试图通过证明极其基本的数学定理来学习伊莎贝尔。这项任务很艰巨,因为出于某种原因,大多数 Isabelle 教程和书籍都侧重于程序分析(列表、树、递归函数)或基本命题/一阶逻辑,其中的练习在很大程度上可以通过(induct_tac "xs")
几个 apply 语句来解决.
然而,通过挖掘现有伊莎贝尔理论的一页又一页,我已经弄清楚了如何定义一些东西。在这种情况下,我定义了一个序列的极限:
theory Exercises
imports Main "Isabelle2019.app/Contents/Resources/Isabelle2019/src/HOL/Rat"
begin
definition limit :: "(nat ⇒ rat) ⇒ rat ⇒ bool"
where limit_def: "limit sequence l = (∃(d::nat). ∀(e::nat)≥d. ∀(ε::rat). abs((sequence d) - l) ≤ ε)"
end
然后我试图证明这一点lim 1/n --> 0
。(抱歉,Latex 不适用于 Stack Overflow)。
我想到的证明很简单:给我一个epsilon
,然后我会告诉你d
一个1/d < epsilon
。但是,在几个最基本的步骤之后,我被困住了。我能得到关于如何完成这个证明的提示吗?
lemma limit_simple: "limit (λ (x::nat). (Fract 1 (int x))) (rat 0)"
unfolding limit_def
proof
fix ε::rat
obtain d_rat::rat where d_rat: "(1 / ε) < d_rat" using linordered_field_no_ub by auto
then obtain d_int::int where d_int: "d_int = (⌊d_rat⌋ + 1)" by auto
then obtain d::nat where "d = max(d_int, 0)"
end
从这个证明的第一行可以看出,我已经被困在试图说服伊莎贝尔相信有一个自然数d
大于1/epsilon
每个有理数epsilon
......
解决方案
首先,你的定义limit
是错误的。你混淆了量词顺序。我会这样写:
definition limit :: "(nat ⇒ rat) ⇒ rat ⇒ bool"
where "limit sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"
然后这里是如何证明你想要的东西:
lemma limit_simple: "limit (λ(x::nat). 1 / of_nat x) 0"
unfolding limit_def
proof (intro allI impI)
fix ε :: rat assume "ε > 0"
obtain d_rat::rat where d_rat: "1 / ε < d_rat" using linordered_field_no_ub by auto
define d where "d = nat (⌊d_rat⌋ + 1)"
have "d_rat ≤ of_nat d"
unfolding d_def by linarith
from ‹ε > 0› have "0 < 1 / ε" by simp
also have "1 / ε < d_rat" by fact
also have "d_rat ≤ of_nat d" by fact
finally have "d > 0" by simp
have "d_rat > 0" using ‹1 / ε > 0› and d_rat by linarith
have "∀e≥d. ¦1 / of_nat e - 0¦ ≤ ε"
proof (intro allI impI)
fix e :: nat
assume "d ≤ e"
have "¦1 / rat_of_nat e - 0¦ = 1 / rat_of_nat e" by simp
have "d_rat ≤ rat_of_nat e"
using ‹d ≤ e› and ‹d_rat ≤ of_nat d› by simp
hence "1 / rat_of_nat e ≤ 1 / d_rat"
using ‹d ≤ e› and ‹d > 0› and ‹d_rat > 0›
by (intro divide_left_mono) auto
also have "1 / d_rat < ε"
using ‹ε > 0› and ‹d_rat > 0› and d_rat by (auto simp: field_simps)
finally show "¦1 / rat_of_nat e - 0¦ ≤ ε" by simp
qed
thus "∃d. ∀e≥d. ¦1 / of_nat e - 0¦ ≤ ε"
by auto
qed
对于实数而不是有理数,证明看起来基本相同。它当然可以自动化一点(好吧,如果你导入 Isabelle 的分析库,它可以在一个步骤中自动证明整个事情)。
在“现实世界”的 Isabelle 中,限制用过滤器表示,并且围绕它们有一个大型库。这使得上述证明陈述变得不那么乏味。
更新:回复您的评论:是的,这有点冗长。在惯用的 Isabelle 中,我会这样写证明:
lemma A: "filterlim (λn. 1 / real n) (nhds 0) sequentially"
proof
fix ε :: real assume "ε > 0"
have "∀⇩F n in sequentially. n > nat ⌈1 / ε⌉"
by (rule eventually_gt_at_top)
hence "∀⇩F n in sequentially. real n > 1 / ε"
by eventually_elim (use ‹ε > 0› in linarith)
moreover have "∀⇩F n in sequentially. n > 0"
by (rule eventually_gt_at_top)
ultimately show "∀⇩F n in sequentially. dist (1 / real n) 0 < ε"
by eventually_elim (use ‹ε > 0› in ‹auto simp: field_simps›)
qed
这个过滤器的概念和一个“最终”持有的属性(这就是这个∀⇩F
语法的意思)非常强大。
更好的是,您可以将上面的证明进一步模块化,首先证明 1/x
趋向于 0 对于x
a real 的 →∞ x
,然后证明对于 a naturalreal n
的 →∞ 趋于实数 ∞ ,然后简单地结合这两个陈述:n
n
lemma B: "filterlim (λx::real. 1 / x) (nhds 0) at_top"
proof
fix ε :: real assume "ε > 0"
have "∀⇩F x in at_top. x > 1 / ε"
by (rule eventually_gt_at_top)
thus "∀⇩F (x::real) in at_top. dist (1 / x) 0 < ε"
using eventually_gt_at_top[of 0]
by eventually_elim (use ‹ε > 0› in ‹auto simp: field_simps›)
qed
lemma C: "filterlim real at_top sequentially"
unfolding filterlim_at_top
proof
fix C :: real
have "∀⇩F n in sequentially. n ≥ nat ⌈C⌉"
by (rule eventually_ge_at_top)
thus "∀⇩F n in sequentially. C ≤ real n"
by eventually_elim linarith
qed
lemma D: "filterlim (λn. 1 / real n) (nhds 0) sequentially"
by (rule filterlim_compose[OF B C])
或者,当然,您可以简单地导入HOL-Real_Asymp.Real_Asymp
,然后所有这些都使用by real_asymp
. ;)
你真的不应该以从头开始做所有事情的难度来判断一个系统,特别是当有一种既定的惯用方式来做这些事情并且你正在积极地做一些不同的事情时。标准库及其习语是系统的重要组成部分。
在证明助手中模仿纸笔式推理是很困难的,尤其是在许多事情是“显而易见的”的渐近学领域。幸运的是,有了一个好的库,确实可以实现某种近似的推理。当然,如果你愿意,你可以进行显式的 ε-δ-推理,但这只会让你的生活更加困难。当我开始在 Isabelle 中使用限制时,我犯了同样的错误(因为 ε-δ 是处理限制的唯一正式方法,我知道而且我不理解所有花哨的过滤器的东西),但是当我开始理解过滤器时更多,事情变得更清晰、更容易、更自然。
推荐阅读
- html - 使用 div 的内联单选按钮
- python - 使用 Pandas 和 Seaborn 绘制多个变量和回归测试
- python - Python pandas 数据框 - 每日数据 - 获取每年的第一天和最后一天
- python-3.x - Python Pillow - 面临crop() 的问题
- kubernetes - 如何创建令牌长度更短的 k8s 服务帐户?
- sql - 如何使 CREATE DATABASE 命令在 SQL 中可重新运行?
- r - 不明白为什么 dplyr 中的填充函数在调用时显示包含该对象的数据集时说该对象不存在
- tinymce - 有没有办法在 Symfony 5.1 中集成 TinyMCE 和 EasyAdmin 3.x Bundle
- javascript - 如何使 axios 获取请求同步?
- java - 每当我尝试登录我的应用程序时,就会发生这些 sql 错误 1146。如何解决?