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 ...
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.