isabelle - 基本伊莎贝尔序列极限证明

Question

正如数百人在我之前尝试过的那样，我正在尝试通过证明极其基本的数学定理来学习伊莎贝尔。这项任务很困难，因为出于某种原因，大多数 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 ...

Answer 1

首先，您对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→ 对于实数 x 趋向于 0 ，然后证明对于 n 来说，real n 趋向于实数 Infinity → 对于自然 n 来说是 Infinity，然后简单地将这两个结合起来声明:

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 中使用极限时，我犯了同样的错误(因为 ε-δ 是处理我所知道的极限的唯一正式方法，而且我不理解所有那些花哨的过滤器的东西)，但是当我开始理解过滤器时，我犯了同样的错误更多，事情变得更清晰、更容易、更自然。