Link between sequential and epsilon/delta versions

Stream: maths

[Ryan Lahfa]

In real analysis, we often encounter sequential version of usual epsilon/delta definitions.

For example, sequential continuity, sequential uniform continuity, accumulation point of a set/sequence, inf/sup.

I have multiple questions Lean and non-Lean ones:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?
(2) It looks like that the equivalence theorem between a sequential version and an epsilon/delta one is also independent of the concept and relies more on the form of the definition rather than on its contents, so, we should be able to produce the equivalence theorem given just a general version of such definitions, right? (under some assumption of choice for sequential → epsilon/delta).
(3) Is this something I could formalize in Lean? Would it be better to go for a type class in such cases?

Maybe, this question is not very relevant because it's impossible to have a general form of sequential version of definitions or things like that.

To give precise examples, here are definitions:

Accumulation point $a$ of a sequence $x$:

Epsilon/Delta: $\forall \varepsilon > 0, \forall n \geq 0, \exists N \geq n, \lvert x_n - a\rvert < \varepsilon$
Sequence form: $\exists y \in x(\mathbb{N})^{\mathbb{N}}, \lim_{n \to +\infty} y_n = a$

Sup:
We say that $a = \sup A$ if:

Epsilon/Delta: $\forall \varepsilon > 0, \exists x \in A, a - \varepsilon < x \leq a$
Sequence form: $\exists y \in A^{\mathbb{N}}, \lim_{n \to +\infty} y_n = a$

Continuity:
We say that $f : A \to B$ is continuous at $x \in A$ if:

Epsilon/delta: $\forall \varepsilon > 0, \exists \delta > 0, \forall y \in A, \lvert x - y \rvert \leq \delta \implies \lvert f(x) - f(y) \rvert \leq \varepsilon$
Sequence form: $\forall x \in A^{\mathbb{N}}, \left(\lim_{n \to +\infty} x_n = x\right) \implies \left(\lim_{n \to +\infty} f(x_n) = f(x)\right)$

[Mario Carneiro]

Filters are the unifying abstraction here

[Mario Carneiro]

In general topological spaces, sequential versions of many concepts exist and are different from the usual ones

[Ryan Lahfa]

Mario Carneiro said:

Filters are the unifying abstraction here

I wanted to avoid those :D… But I guess this is it

[Mario Carneiro]

Given a sequence there is a filter defined by "containing cofinitely many of the points of the sequence", and a limit of the filter is the same as a limit of the sequence

[Mario Carneiro]

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of \all x, \exists y, P x y with \ex f, \forall x, P x (f x)

[Ryan Lahfa]

Mario Carneiro said:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of \all x, \exists y, P x y with \ex f, \forall x, P x (f x)

Okay, I was remembering something in terms of "skolemization" and logic, but could not find what I needed. Thank you so much!

[Mario Carneiro]

although in order to make them sequences there is an additional step where you weaken the real number epsilon quantifier to an equivalent natural number quantifier

[Mario Carneiro]

(which is where the difference is in general, non first countable topological spaces)

[Ryan Lahfa]

Okay, it makes a lot of sense now, thank you!

[Ryan Lahfa]

Mario Carneiro said:

(1) It looks like we can often write a dual sequential version of many epsilon/delta definitions, is there a name for this? Is there a concept? Can we give a "normal form" to those definitions?

Actually, the logical manipulation you are doing to the definitions to get this is well known elsewhere as "skolemization", the interchanging of \all x, \exists y, P x y with \ex f, \forall x, P x (f x)

BTW, is there any skolemization lemma in Lean?

[Alex J. Best]

classical.skolem in core lean?

[Kevin Buzzard]

If you're formalising analysis in tactic mode you might never need to use terms such as this though

[Ryan Lahfa]

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

[Ryan Lahfa]

My problem is I often run into those dual definitions when I'm attempting to proof stuff.

And, when let's say I have a proof of having an accumulation point in an epsilon/delta-style, I'm not sure how to convert it into a sequence-style proof easily without writing a lot of machinery (?).

[Patrick Massot]

You shouldn't be afraid of filters. They are much nicer than epsiloneries.

[Ryan Lahfa]

Patrick Massot said:

You shouldn't be afraid of filters. They are much nicer than epsiloneries.

All the contrary, I love them; but I am not allowed to use them because of most students (and maybe non-topologists teachers) which do not understand them very well

But at the same time, I'm frustrated with repeating the same boring & technical proofs…

[Kevin Buzzard]

Ryan Lahfa said:

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

Because we have tactics like choose.

[Ryan Lahfa]

Kevin Buzzard said:

Ryan Lahfa said:

Kevin Buzzard said:

If you're formalising analysis in tactic mode you might never need to use terms such as this though

Why?

Because we have tactics like choose.

Wow. That's awesome!

[Ryan Lahfa]

Though, I come back with an MWE because I didn't succeed to make choose work well.

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

def converge (x: ℕ → X) (l : X) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)

lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X):
  S.nonempty → bdd_above S → ∃ (x: ℕ → X), (set.range x) ⊆ S ∧ converge x (Sup S) := begin
  intros hnn hbdd,
  end

Let's say I want to prove that sup_is_a_cv_seq, so ideally, I should be able to reuse some parts of mathlib, namely cSup_intro I imagine and taking ϵ = 1/n for all n ≥ 0, this way, I should be able to have this lemma easily w/o rewriting a lot of stuff, right?

[Ryan Lahfa]

Specifically, if I try to do this:

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

def converge (x: ℕ → X) (l : X) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)

lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X):
  S.nonempty → bdd_above S → ∃ (x: ℕ → X), (set.range x) ⊆ S ∧ converge x (Sup S) := begin
  intros hnn hbdd,
  have: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := sorry,
  have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := sorry,

  choose x hrange h using this,
  use x,
  split,
  intros y hy,
  obtain ⟨ N, hN ⟩ := hy,
  rw ← hN,
  exact hrange N,
  intros ε hε,
  -- 1/(N + 1) ≤ eps
  -- 1/eps ≤ N + 1
  -- 1/eps - 1 ≤ N
  -- use (floor(1/eps - 1) + 1)
  use (floor((1/ϵ) - 1) + 1),


  end

The use won't work.

[Ryan Lahfa]

Because floor is in Z and I have to prove that the total value is in N, I guess.

[Ryan Lahfa]

Huh, no, the code provided uses a ϵ and the ε is not the same…

[Ryan Lahfa]

Wonder if it is my CPU or something, but:

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x=y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

def converge (x: ℕ → X) (l : X) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)

lemma sup_is_a_cv_seq [conditionally_complete_linear_order X] (S: set X):
  S.nonempty → bdd_above S → ∃ (x: ℕ → X), (set.range x) ⊆ S ∧ converge x (Sup S) := begin
  intros hnn hbdd,
  have: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := sorry,
  have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := sorry,
  choose x hrange h using this,
  use x,
  split,
  intros y hy,
  obtain ⟨ N, hN ⟩ := hy,
  rw ← hN,
  exact hrange N,
  intros ε hε,
  -- 1/(N + 1) ≤ eps
  -- 1/eps ≤ N + 1
  -- 1/eps - 1 ≤ N
  -- use (floor(1/eps - 1) + 1)
  set N₀ := (floor((1/ε) - 1) + 1),
  have N0_pos: N₀ ≥ 0 := sorry,
  -- lift N₀ to ℕ using N0_pos,
  use N₀,

  sorry,
  end

is taking a lot of time to compute.

[Kevin Buzzard]

presep could be less clunkily expressed as forall x, d x x = 0, and d_pos follows from triangle and sym and presep

[Ryan Lahfa]

Kevin Buzzard said:

presep could be less clunkily expressed as forall x, d x x = 0, and d_pos follows from triangle and sym and presep

Thank you!

[Kevin Buzzard]

I am concerned about your first sorry

[Mario Carneiro]

at the risk of pointing out the obvious, mathlib already has a definition of metric spaces

[Kevin Buzzard]

But what about a metric space which is also a conditionally complete linear order?

[Kevin Buzzard]

Because I am concerned that these two structures, the way you have set things up, are completely unrelated.

[Ryan Lahfa]

Mario Carneiro said:

at the risk of pointing out the obvious, mathlib already has a definition of metric spaces

I know, this is rather to have another metric space definition which does not use filters, but only standard sequences.

[Mario Carneiro]

but the definition doesn't say anything about sequences

[Kevin Buzzard]

For example I don't see any reason why Sup S (which is defined using the complete linear order structure) should have anything to do with converge (which is defined using he metric space)

[Ryan Lahfa]

Kevin Buzzard said:

Because I am concerned that these two structures, the way you have set things up, are completely unrelated.

Yes, I definitely feel super wrong about this too. But in order to talk about Sup, I need some structure where bounded above gives me a sup.

[Kevin Buzzard]

Sure, but you haven't glued your two choices of structure together

[Ryan Lahfa]

Kevin Buzzard said:

For example I don't see any reason why Sup S (which is defined using the complete linear order structure) should have anything to do with converge (which is defined using he metric space)

Wouldn't cSup_intro give me the first sorry?

[Kevin Buzzard]

You can't prove any theorem relating sups to distances here

[Ryan Lahfa]

Mario Carneiro said:

but the definition doesn't say anything about sequences

Of metric spaces?

[Ryan Lahfa]

Kevin Buzzard said:

You can't prove any theorem relating sups to distances here

I see what you mean, right.

[Mario Carneiro]

I think you want to know that the topology is orderable

[Kevin Buzzard]

You have currently written "Let $X$ be a metric space. Assume also that $X$ has a total order, which is completely unrelated to the metric space structure. Then..."

[Mario Carneiro]

but that requires the topology of the metric space, so at that point you are better off using the mathlib definition

[Mario Carneiro]

You can probably recast it in terms of compatibility directly, something like "intervals contain open balls and vice versa"

[Ryan Lahfa]

Let's assume I want to prove this only for $\mathbb{R}$ right now, so the first sorry is not a problem anymore, right? I can just remove the total orderable condition.

[Ryan Lahfa]

Okay, I see now why the first sorry was not feasible, indeed.

[Kevin Buzzard]

If you don't want to work with $\mathbb{R}$ directly you need to come up with some structure where the ideas you want to formalise are still true, and it sounds to me like you want the topology induced by the metric to equal the topology induced by the order.

[Kevin Buzzard]

So either you formalise what the topology induced by your metric is, or you use mathlib metric spaces where it's already there.

[Ryan Lahfa]

I'll directly work with $\mathbb{R}$ right now because I won't use this lemma for something else than $\mathbb{R}$.
After I succeed, I'll revisit it to improve it with the topology order condition rather.

[Ryan Lahfa]

My whole code becomes now:

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x = y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

instance real.metric_space : metric_space ℝ :=
{ d                  := λx y, abs (x - y),
  d_pos              := by simp [abs_nonneg],
  presep             := begin simp, apply sub_eq_zero_of_eq end,
  sep                := begin simp, apply eq_of_sub_eq_zero end,
  sym                := assume x y, abs_sub _ _,
  triangle           := assume x y z, abs_sub_le _ _ _ }

theorem real.dist_eq (x y : ℝ) : d x y = abs (x - y) := rfl

theorem real.dist_0_eq_abs (x : ℝ) : d x 0 = abs x :=
by simp [real.dist_eq]

def converge (x: ℕ → X) (l : X) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)


lemma sup_is_a_cv_seq (S: set ℝ):
  S.nonempty → bdd_above S → ∃ (x: ℕ → ℝ), (set.range x) ⊆ S ∧ converge x (Sup S) := begin
  intros hnn hbdd,
  have: ∀ ε > 0, ∃ x ∈ S, Sup S - x < ε := sorry,
  have: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := begin
  intros ε hε,
  obtain ⟨ x, hx, hs_lt ⟩ := this ε hε,
  use x,
  split,
  exact hx,
  rw real.dist_eq,
  apply abs_lt_of_lt_of_neg_lt,
  exact hs_lt,
  sorry, -- by definition of sup.
  end,
  have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := sorry,
  choose x hrange h using this,
  use x,
  split,
  intros y hy,
  obtain ⟨ N, hN ⟩ := hy,
  rw ← hN,
  exact hrange N,
  intros ε hε,
  -- 1/(N + 1) ≤ eps
  -- 1/eps ≤ N + 1
  -- 1/eps - 1 ≤ N
  lift floor(1/ε) to ℕ with N₀,
  use N₀,
  intros n hn,
  transitivity,
  exact h n,
  sorry,
  end

[Kevin Buzzard]

I can't find orderable in mathlib by the way

[Kevin Buzzard]

Do you have a question or are you now OK to keep going?

[Ryan Lahfa]

I think I can now finish the proof by myself —but feel free if you see stupid things (except the fact I'm writing my own metric_space def which is only for the sake of exercise.)

[Kevin Buzzard]

Your proof looks just like the kind of proofs I was writing when I was learning.

[Ryan Lahfa]

I definitely abuse of have because I'm trying to see how it works, but I clean up afterwards to have something more natural

[Ryan Lahfa]

Other than this, I think I might be using obtain in a suboptimal way sometimes, and I'm not sure by what I should replace it

[Ryan Lahfa]

transitivity is cool because it expresses 1:1 how I think, but those meta variables are not good I guess ; also, it does not work when I want to do: a ≤ b < c — I don't know what good replacement there would be for this? (I could chain the right lemmas given enough time, but it's somewhat annoying)

[Kevin Buzzard]

lt_of_le_of_lt

[Ryan Lahfa]

I should try to have the confidence to write those directly as they're so natural…

[Mario Carneiro]

it's actually order_topology

[Mario Carneiro]

I think the names changed at some point; there is order_topology and order_closed_topology now

[Reid Barton]

I also distinctly remember something about orderable

[Scott Morrison]

You can also use calc blocks instead of transitivity, or having the confidence to write lt_of_le_of_lt.

[Scott Morrison]

calc blocks also have the advantage of readability (as long as the proof terms on each line stay succinct).

[Patrick Massot]

Ryan, do you know that transitivity can take an argument instantiating the meta-variable you complain about?

[Patrick Massot]

I still agree with Scott that you should probably be using more calc blocks. linarith can also get rid of all this as long as you state the relevant fact before, or pass them to linarith.

[Ryan Lahfa]

@Patrick Massot I didn't know and I should have tried, I assumed that transitivity didn't take any argument, thanks.

[Patrick Massot]

Your lemma sup_is_a_cv_seq was the end goal of my Lean L1 course last year.

[Ryan Lahfa]

Patrick Massot said:

I still agree with Scott that you should probably be using more calc blocks. linarith can also get rid of all this as long as you state the relevant fact before, or pass them to linarith.

I'll give a try to calc blocks, they look like more natural to me.

[Patrick Massot]

But you are not approaching it in the right Lean mindset. You need to write the proof on paper, and collect all the « obvious facts » used in the proof. Them write lemmas about those obvious facts.

[Kenny Lau]

I don't like (set.range x) ⊆ S because it is harder to prove and use than \forall n, x n \in S

[Patrick Massot]

Yes, I wanted to write this also.

[Ryan Lahfa]

Patrick Massot said:

Your lemma sup_is_a_cv_seq was the end goal of my Lean L1 course last year.

Oh wow, ideally, I'd like to generalize it to orderable topologies, like I'd been advised by @Mario Carneiro (behind this, I'm proving the classical Bolzano-Weierstrass)

[Patrick Massot]

set.range and set.image are evil. They look nice on paper because you automatically do the required bureaucracy in your head without noticing.

[Patrick Massot]

Sorry, I meant "of the exam of my Lean L1 course".

[Ryan Lahfa]

Patrick Massot said:

set.range and set.image are evil. They look nice on paper because you automatically do the required bureaucracy in your head without noticing.

Kenny Lau said:

I don't like (set.range x) ⊆ S because it is harder to prove and use than \forall n, x n \in S

Alright, but stating \forall n, x n \in S looks like a bit weird when in reality what I want to express is that the image of the sequence is a subset of S

[Patrick Massot]

I forgot part of the sentence.

[Ryan Lahfa]

Patrick Massot said:

I forgot part of the sentence.

Patrick Massot said:

Sorry, I meant "of the exam of my Lean L1 course".

Ah! Is it available somewhere? I'm quite interested into this!

[Patrick Massot]

No, you want to express that the sequence takes values in S.

[Patrick Massot]

You would never say "the image of the sequence is a subset of S".

[Ryan Lahfa]

Indeed, I agree

[Ryan Lahfa]

But I'd just write $(x_n)_n \in S^{\mathbb{N}}$

[Kenny Lau]

but whenever you prove / use this sentence you always prove that $x_n \in S \forall n$

[Patrick Massot]

Ryan Lahfa said:

But I'd just write $(x_n)_n \in S^{\mathbb{N}}$

You shouldn't. Really.

[Ryan Lahfa]

Patrick Massot said:

Ryan Lahfa said:

But I'd just write $(x_n)_n \in S^{\mathbb{N}}$

You shouldn't. Really.

What would you advise to write?

[Patrick Massot]

Anyway, you should have lemma saying ∀ ε > 0, ∃ x ∈ S, Sup S - ε < x outside from your main proof. And then the same with 1/(N+1) instead of ε.

[Ryan Lahfa]

Patrick Massot said:

Anyway, you should have lemma saying ∀ ε > 0, ∃ x ∈ S, Sup S - ε < x outside from your main proof. And then the same with 1/(N+1) instead of ε.

Yes, I was planning to extract those as they're looking like lemmas on themselves.

[Patrick Massot]

And a lemma saying that if for all n, d (x n) l < 1/(N+1) then x converges to l.

[Patrick Massot]

Because these all lemmas that are "obvious" when you have already reached the point where you want to prove this Sup thing.

[Patrick Massot]

So you don't want to be proving them in the middle of this proof.

[Patrick Massot]

You wouldn't do that on paper and you wouldn't do that in Lean.

[Patrick Massot]

And of course a lemma saying that 1/(N+1) is less than any epsilon for N large enough

[Ryan Lahfa]

Definitely.

[Ryan Lahfa]

Would one_div_lt_epsilon be a right name for the last lemma?

[Ryan Lahfa]

For forall n, d (x n) l < 1/(N + 1) → converge x l, I'm not sure how to call it except convergence_aux_1

[Patrick Massot]

converge_of_dist_lt_one_div_succ?

[Kenny Lau]

converge_of_d_lt

[Ryan Lahfa]

I tried to take into account most of your advice and came back with this:

import data.set
import data.set.finite
import data.real.basic
import data.finset
import order.conditionally_complete_lattice

noncomputable theory
open_locale classical
open set

class metric_space (X : Type) :=
(d : X → X → ℝ)
(d_pos : ∀ x y, d x y ≥ 0)
(presep : ∀ x y, x = y → d x y = 0)
(sep : ∀ x y, d x y = 0 →  x = y)
(sym : ∀ x y, d x y = d y x)
(triangle : ∀ x y z, d x z ≤ d x y + d y z)

variables {X:Type} [metric_space X]

open metric_space

instance real.metric_space : metric_space ℝ :=
{ d                  := λx y, abs (x - y),
  d_pos              := by simp [abs_nonneg],
  presep             := begin simp, apply sub_eq_zero_of_eq end,
  sep                := begin simp, apply eq_of_sub_eq_zero end,
  sym                := assume x y, abs_sub _ _,
  triangle           := assume x y z, abs_sub_le _ _ _ }

theorem real.dist_eq (x y : ℝ) : d x y = abs (x - y) := rfl

theorem real.dist_0_eq_abs (x : ℝ) : d x 0 = abs x :=
by simp [real.dist_eq]

def converge (x: ℕ → X) (l : X) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, ((d l (x n))  < ε)

lemma real.sup_sub_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, Sup S - x < ε := sorry
lemma real.sup_dist_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := begin
  intros ε hε,
  obtain ⟨ x, hx, hs_lt ⟩ := real.sup_sub_lt_eps ε hε,
  use x,
  split,
  exact hx,
  rw real.dist_eq,
  apply abs_lt_of_lt_of_neg_lt,
  exact hs_lt,
  sorry,
end

lemma converge_of_dist_lt_one_div_succ {x: ℕ → ℝ} {l: ℝ}: (∀ n, d l (x n) ≤ 1 / (n + 1)) → converge x l := begin
intro H,
intros ε hε,
obtain ⟨ N, hN ⟩ := exists_nat_one_div_lt hε,
use N,
intros n hn,
calc d l (x n) ≤ 1 / (n + 1) : H n
    ... ≤ 1 / (N + 1) : nat.one_div_le_one_div hn
    ... < ε : hN
end

lemma sup_is_a_cv_seq (S: set ℝ):
  S.nonempty → bdd_above S → ∃ (x: ℕ → ℝ), (∀ n, x n ∈ S) ∧ converge x (Sup S) := begin
  intros hnn hbdd,
  have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x < 1/(N + 1) := begin
  intro N,
  apply real.sup_dist_lt_eps,
  apply nat.one_div_pos_of_nat,
  end,
  choose x hrange h using this,
  use x,
  split,
  exact hrange,
  exact converge_of_dist_lt_one_div_succ h, -- this line should work (?)
  end

But, I have some issue regarding the types, here is the state at the last step:

type mismatch at application
  converge_of_dist_lt_one_div_succ h
term
  h
has type
  ∀ (N : ℕ), d (Sup S) (x N) < 1 / (↑N + 1)
but is expected to have type
  ∀ (n : ℕ), d (Sup S) (x n) ≤ 1 / (↑n + 1)
state:
S : set ℝ,
hnn : set.nonempty S,
hbdd : bdd_above S,
x : ℕ → ℝ,
hrange : ∀ (N : ℕ), x N ∈ S,
h : ∀ (N : ℕ), d (Sup S) (x N) < 1 / (↑N + 1)
⊢ converge x (Sup S)

I'm not sure what is actually different except some typeclasses, I tried to print those with set_option pp.all true but got lost as there were a huge amount of those.

[Kevin Buzzard]

You have a < in one and a <=in the other

[Ryan Lahfa]

Thanks…

[Ryan Lahfa]

@Kevin Buzzard Is there a way to apply le_of_lt in this part:

  have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x ≤ 1/(N + 1) := begin
  intro N,
  apply le_of_lt, -- won't work because of exists
  apply real.sup_dist_lt_eps,
  apply nat.one_div_pos_of_nat,
  end,

?

[Kevin Buzzard]

Instead of apply use convert maybe. What is the type of real.sup_dist_lt_pos?

[Ryan Lahfa]

Kevin Buzzard said:

Instead of apply use convert maybe. What is the type of real.sup_dist_lt_pos?

lemma real.sup_dist_lt_eps {S: set ℝ}: ∀ ε > 0, ∃ x ∈ S, d (Sup S) x < ε := begin

[Kevin Buzzard]

Make a term which starts with an exists from that term and convert it

[Kevin Buzzard]

Ie supply the correct epsilon

[Kevin Buzzard]

Hmm this still won't work

[Reid Barton]

right, it won't work because le_of_lt is not an equality

[Ryan Lahfa]

I tried this: convert real.sup_dist_lt_eps (1 / (N + 1)) (nat.one_div_pos_of_nat),

[Kevin Buzzard]

Well just do cases on the term to get to an epsilon

[Kevin Buzzard]

Convert won't work

[Reid Barton]

You need to know if $P(x) \implies Q(x)$ for all x, then $(\exists x, P(x)) \implies (\exists x, Q(x))$ and we don't have a general framework for that

[Reid Barton]

If it was $=$ and not $\implies$ then you could use convert or conv or whatever.

[Kevin Buzzard]

Do cases on the term you make with the exists and use that x

[Kevin Buzzard]

Or just apply the logic lemma. Presumably it's in logic.basic?

[Ryan Lahfa]

Kevin Buzzard said:

Well just do cases on the term to get to an epsilon

Is this something like this: cases (real.sup_dist_lt_eps (1 / (N + 1)) (nat.one_div_pos_of_nat)) with x hx, often?

[Kevin Buzzard]

If you got an x and an hx that looks good then yes. You might be better off with rcases though

[Kevin Buzzard]

Because you want to extract x in S and not just x

[Ryan Lahfa]

Is there a preference between rcases and obtain?

[Ryan Lahfa]

Because I often use obtain to extract arbitrary complex constructors

[Kevin Buzzard]

Obtain is best

[Ryan Lahfa]

This works:

  have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x ≤ 1/(N + 1) := begin
  intro N,
  obtain ⟨ x, hrange, hsup ⟩ := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat)),
  use x,
  split,
  exact hrange,
  apply le_of_lt,
  exact hsup,
  end,

anyway

[Kevin Buzzard]

I always forget about it because it's relatively new

[Ryan Lahfa]

Thanks!

[Kevin Buzzard]

Now can you write it in pure term mode?

[Kevin Buzzard]

lambda instead of intro etc?

[Kevin Buzzard]

There are no serious tactics in your code so you don't need tactic mode at all

[Kevin Buzzard]

Obtain becomes let ... in

[Kevin Buzzard]

Split is pointy brackets

[Kevin Buzzard]

And exact can be removed completely

[Ryan Lahfa]

I started like this: λ N, let ⟨ x, hrange, hsup ⟩ in (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat)),

[Ryan Lahfa]

But it is complaining about the syntax — I guess I'm doing something wrong

[Ryan Lahfa]

Huh, yes let x := t in s

[Patrick Massot]

Your use of obtain make it completely equivalent to rcases. This is fine, but you should know the added value of obtain is you can write the expected type upfront.

[Patrick Massot]

In your case that would be purely for readability purposes.

[Ryan Lahfa]

Patrick Massot said:

Your use of obtain make it completely equivalent to rcases. This is fine, but you should know the added value of obtain is you can write the expected type upfront.

I see, I can do obtain <pattern>: type := … and I can omit <pattern> ?

[Ryan Lahfa]

@Kevin Buzzard I'm not sure how to replace the use x; (also is there any docs for the commands for the pointy brackets, etc. ?)

[Patrick Massot]

You can do a lot of things:

  obtain ⟨x, hx⟩ : ∃ x, P x,
  { long proof... },
  obtain ⟨x, hx⟩ : ∃ x, P x := proof_term,
  obtain ⟨x, hx⟩ : ∃ x, P x, from proof_term,

[Patrick Massot]

Only the first case really needs obtain rather than rcases. But all are more readable than rcases

[Patrick Massot]

And of course you can get the same with have + rcases but you'd get tired of this pretty quickly.

[Ryan Lahfa]

Makes sense, is there any docs to write tactics? I'm understanding more and more how to compose all of this and I'm interested in how it works

[Kevin Buzzard]

Beginning tactic writing is covered in a doc which Patrick wrote in the docs directory of mathlib

[Ryan Lahfa]

Now I'm this far:

have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x ≤ 1/(N + 1) := λ N,
  let ⟨ x, ha, hb ⟩ := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat))
  in exists.intro x (λ hp, and.intro (...) (...) ),

Is it expected that Lean VSCode cannot print the current state in term mode?

[Kevin Buzzard]

Use X is just <X,_> with the right brackets

[Bhavik Mehta]

By the way, can we make VSCode highlight obtain (and set) the same way as have (and let)?

[Reid Barton]

Use _ where you have (...), and then hover over it, or something (I use emacs, but I assume vscode can do this too)

[Gabriel Ebner]

@Bhavik Mehta Feel free to PR a change to this file: https://github.com/leanprover/vscode-lean/blob/9a4400a1f3db57d0a25c1944812b0c2dc9ff2141/syntaxes/lean.json#L35 But I wouldn't highlight set: this occurs often as a non-tactic, e.g. in set α.

[Ryan Lahfa]

Indeed, it works when I use _, now I have this state:

context:
S : set ℝ,
hnn : set.nonempty S,
hbdd : bdd_above S,
N : ℕ,
_let_match :
  (∃ (x : ℝ) (H : x ∈ S), d (Sup S) x < 1 / (↑N + 1)) →
  (∃ (x : ℝ) (H : x ∈ S), d (Sup S) x ≤ 1 / (↑N + 1)),
x : ℝ,
ha : x ∈ S,
hb : d (Sup S) x < 1 / (↑N + 1)
⊢ ∃ (H : x ∈ S), d (Sup S) x ≤ 1 / (↑N + 1)

But the exists in front of this is strange? I'm not sure how I can combine ha/hb to finish

[Bhavik Mehta]

Gabriel Ebner said:

Bhavik Mehta Feel free to PR a change to this file: https://github.com/leanprover/vscode-lean/blob/9a4400a1f3db57d0a25c1944812b0c2dc9ff2141/syntaxes/lean.json#L35 But I wouldn't highlight set: this occurs often as a non-tactic, e.g. in set α.

Thanks! Ah yeah good point

[Ryan Lahfa]

have: ∀ (N: ℕ), ∃ x ∈ S, d (Sup S) x ≤ 1/(N + 1) := λ N,
  let ⟨ x, ha, hb ⟩ := (real.sup_dist_lt_eps S (1 / (N + 1)) (nat.one_div_pos_of_nat))
  in ⟨ x, ⟨ ha, le_of_lt hb ⟩ ⟩,

This seems to work!

[Ryan Lahfa]

Thank you for the tip! I have seen symbols like ▸ , what does that mean? I see it in mathlib sometimes, but I didn't find any docs on it

[Reid Barton]

ah, the dreaded "stupid triangle"

[Patrick Massot]

also known by its full name as the dreaded "I'm-sorry-but-I-don't-know-the-expected-type triangle".

[Reid Barton]

if p : P a and e : a = b then e ▸ p : P b, except it basically never manages to work out what P should be

[Reid Barton]

it's like a term-mode version of rw that rarely works

[Ryan Lahfa]

Oh okay

[Patrick Massot]

You get extra credit when you manage to use it in a proof.

[Ryan Lahfa]

Hahahaha

[Kevin Buzzard]

Good job for getting the term!

[Kevin Buzzard]

One thing to remember about the stupid triangle is that in contrast to tactic mode it has to be told all inputs , ie rw add_comm works but with the triangle you might have to put add_comm a b