基本伊莎贝尔序列极限证明
Basic Isabelle sequence limit proof
在我之前已经有数百人尝试过，我正在尝试通过证明极其基本的数学定理来学习伊莎贝尔。这项任务很难，因为出于某种原因，大多数 Isabelle 教程和书籍都侧重于程序分析（列表、树、递归函数）或基本 propositional/first-order 逻辑，其中的练习在很大程度上可以通过 (induct_tac "xs") 和几个应用语句。
但是，通过翻阅现有的 Isabelle 理论的页面和页面，我已经想出了如何定义某些东西。在这种情况下，我定义了一个序列的极限：
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 中，我会这样写证明：
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 对于 x 趋向于 0 → ∞ 对于实数 x，然后表明 real 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 中使用极限时，我犯了同样的错误（因为 ε-δ 是处理我所知道的极限的唯一正式方法，而我并不理解所有那些花哨的过滤器），但是当我开始理解过滤器时更多，事情变得更清晰、更容易、更自然。
我认为这里的很多困难来自nat和rat之间的所有转换。在有理数上证明等价函数的极限更容易：
definition limit_r :: "(rat ⇒ rat) ⇒ rat ⇒ bool"
where "limit_r sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"
lemma limit_simple_r: "limit_r (λx. 1 / x) 0"
unfolding limit_r_def
proof (intro allI impI)
fix ε :: rat assume "ε > 0"
hence "¦1 / (1/ε) - 0¦ ≤ ε"
by auto
hence "∀e≥(1/ε). ¦1 / e - 0¦ ≤ ε"
using `ε > 0` by (auto simp add: divide_le_eq order_trans )
thus "∃d. ∀e≥d. ¦1 / e - 0¦ ≤ ε"
by blast
qed
然后可以将结果转回序列：
definition limit :: "(nat ⇒ rat) ⇒ rat ⇒ bool"
where "limit sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"
lemma to_rat_limit:
assumes a1: "limit_r sequence_r l"
and a2: "⋀n. sequence n = sequence_r (of_nat n)"
shows "limit sequence l"
unfolding limit_def proof (intro allI impI)
fix ε :: rat
assume "0 < ε"
from assms obtain d where "∀e≥d. ¦sequence_r e - l¦ ≤ ε"
using ‹0 < ε› using limit_r_def by blast
hence "¦sequence e - l¦ ≤ ε" if "e ≥ nat ⌈d⌉" for e
using that a2 by (auto, meson of_nat_ceiling of_nat_mono order_trans)
thus "∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε"
by blast
qed
lemma limit_simple: "limit (λ(x::nat). 1 / of_nat x) 0"
using limit_simple_r to_rat_limit by auto
在我之前已经有数百人尝试过，我正在尝试通过证明极其基本的数学定理来学习伊莎贝尔。这项任务很难，因为出于某种原因，大多数 Isabelle 教程和书籍都侧重于程序分析（列表、树、递归函数）或基本 propositional/first-order 逻辑，其中的练习在很大程度上可以通过 (induct_tac "xs") 和几个应用语句。
但是，通过翻阅现有的 Isabelle 理论的页面和页面，我已经想出了如何定义某些东西。在这种情况下，我定义了一个序列的极限：
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 中，我会这样写证明：
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 对于 x 趋向于 0 → ∞ 对于实数 x，然后表明 real 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 中使用极限时，我犯了同样的错误（因为 ε-δ 是处理我所知道的极限的唯一正式方法，而我并不理解所有那些花哨的过滤器），但是当我开始理解过滤器时更多，事情变得更清晰、更容易、更自然。
我认为这里的很多困难来自nat和rat之间的所有转换。在有理数上证明等价函数的极限更容易：
definition limit_r :: "(rat ⇒ rat) ⇒ rat ⇒ bool"
where "limit_r sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"
lemma limit_simple_r: "limit_r (λx. 1 / x) 0"
unfolding limit_r_def
proof (intro allI impI)
fix ε :: rat assume "ε > 0"
hence "¦1 / (1/ε) - 0¦ ≤ ε"
by auto
hence "∀e≥(1/ε). ¦1 / e - 0¦ ≤ ε"
using `ε > 0` by (auto simp add: divide_le_eq order_trans )
thus "∃d. ∀e≥d. ¦1 / e - 0¦ ≤ ε"
by blast
qed
然后可以将结果转回序列：
definition limit :: "(nat ⇒ rat) ⇒ rat ⇒ bool"
where "limit sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"
lemma to_rat_limit:
assumes a1: "limit_r sequence_r l"
and a2: "⋀n. sequence n = sequence_r (of_nat n)"
shows "limit sequence l"
unfolding limit_def proof (intro allI impI)
fix ε :: rat
assume "0 < ε"
from assms obtain d where "∀e≥d. ¦sequence_r e - l¦ ≤ ε"
using ‹0 < ε› using limit_r_def by blast
hence "¦sequence e - l¦ ≤ ε" if "e ≥ nat ⌈d⌉" for e
using that a2 by (auto, meson of_nat_ceiling of_nat_mono order_trans)
thus "∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε"
by blast
qed
lemma limit_simple: "limit (λ(x::nat). 1 / of_nat x) 0"
using limit_simple_r to_rat_limit by auto