Basic Isabelle sequence limit proof

Question

As hundreds have tried before me, I'm trying to learn Isabelle by attempting to prove extremely basic mathematical theorems. The task is hard because most Isabelle tutorials and books focus, for some reason, on program analysis (lists, trees, recursive functions) or elementary propositional/first-order logic and the exercises therein can largely be solved by (induct_tac "xs") and a couple of apply statements.

However, by digging through pages and pages of existing Isabelle theories, I have figured out how to define something. In this case, I defined the limit of a sequence:

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

Then I tried to prove that lim 1/n --> 0. (sorry, Latex doesn't work on Stack Overflow).

The proof I had in mind was quite simple: give me an epsilon, and I'll show you a d after which 1/d < epsilon. However, I'm stuck after a couple of most basic steps. Could I get a hint on how to complete this proof?

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

As maybe visible from the very first lines of this proof, I am already stuck trying to convince Isabelle that there is a natural number d that is greater than 1/epsilon for every rational epsilon ...

Answer 1

I think a lot of the difficulties here come from all the conversions between nat and rat. It is easier to prove the limit for an equivalent function on the rationals:

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

The results can then be transferred back to sequences:

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

Answer 2

First of all, your definition of limit is wrong. You mixed up the quantifier order a bit. Here's how I would write it:

definition limit :: "(nat ⇒ rat) ⇒ rat ⇒ bool"
  where "limit sequence l = (∀ε>0. ∃d. ∀e≥d. ¦sequence e - l¦ ≤ ε)"

And then here is how one could prove the thing you wanted:

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

The proof would look basically the same for real numbers instead of rational ones. It could certainly be automated a bit more (well, if you import Isabelle's analysis library, it can prove the entire thing automatically in a single step).

In ‘real world’ Isabelle, limits are expressed with filters, and there is a large library around them. This makes proving statements such as the above much less tedious.

Update: Responding to your comment: Yes, this is a bit lengthy. In idiomatic Isabelle, I would write the proof something like this:

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

This concept of filters and a property holding ‘eventually’ (that's what this ∀⇩F syntax means) is very powerful.

Even better, you can modularise the above proof a bit more into first showing that 1/x tends to 0 for x→∞ for a real x, and then show that real n tends to real ∞ for n→∞ for a natural n and then simply combine these two statements:

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])

Or, of course, you can simply import HOL-Real_Asymp.Real_Asymp and then all of these are done automatically using by real_asymp. ;)

You really should not judge a system by how difficult it is to do everything from scratch, especially when there is an established idiomatic way of how to do them and you are actively doing something different. The standard library and its idioms are an important part of the system.

It is difficult to emulate pen-and-paper-style reasoning in a proof assistant, especially in an area like asymptotics where many things are ‘obvious’. Luckily, with a good library, some approximation of that kind of reasoning can indeed be achieved. You can do explicit ε-δ-reasoning if you want to, of course, but it's just going to make your life more difficult. I made the same mistake when I started working with limits in Isabelle (because ε-δ is the only formal way to treat limits that I knew and I didn't understand all that fancy filter stuff), but as soon as I started understanding filters more, things became much clearer, easier, and more natural.