Recursively defined sequence within proof

Stream: new members

[Heather Macbeth]

How do I define a sequence recursively within a larger tactic mode proof? Say I want to prove the following theorem:

import data.real.basic

/-- Definition of the limit of a sequence -/
def converges_to (x : ℕ → ℝ) (X : ℝ) : Prop :=
∀ ε > 0, ∃ (M : ℕ), ∀ (n ≥ M), abs (x n - X) < ε

/-- If `s` is nonempty and bounded above, and does not contain its supremum `l`, then there
exists a strictly monotone sequence of elements of `s` which converges to `l`. -/
example (s : set ℝ) [nonempty s] {l : ℝ} (hl : is_lub s l) (hl' : l ∉ s) :
  ∃ x : ℕ → s, strict_mono x ∧ converges_to (coe ∘ x) l :=
sorry

The proof should go like this: We construct the sequence recursively. Define x 0 to be an arbitrary element of s. Then, given that x k is defined, we have x k < l since l ∉ s, so max (x k) (l - 1 / (k + 1)) is not an upper bound for s and so there exists some element of s greater than this max, which I define to be x (k + 1).

How can I set this up? I think I have found the right section of #tpil
https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#structural-recursion-and-induction
but I don't know how to make a "throwaway" recursive definition within a larger tactic mode proof.

[Floris van Doorn]

I would define an auxilliary noncomputable definition that takes an element of s (and the rest of the data) and returns the next element in the sequence.
Then x n is just aux^[n] (x 0)

[Floris van Doorn]

Then proving basic properties about aux also immediately splits up one large proof in many small ones.

[Floris van Doorn]

If you really want a single proof, I would do the same, but use let aux := ...

[Heather Macbeth]

I see, so the nice syntax at
https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#structural-recursion-and-induction
with

def fib : nat → nat
| 0     := 1
| 1     := 1
| (n+2) := fib (n+1) + fib n

is completely irrelevant to what I want to do?

[Floris van Doorn]

Yeah, the equation compiler doesn't seem necessary at all for this purpose.
If the function was going to be more complicated, and you did want to use the equation compiler, then the same advice still applies: split up the proof so that you define a top-level definition with the equation compiler, and then prove properties about it, before you actually begin the proof of the main theorem.

[Heather Macbeth]

OK, thanks! Let me try this method and see if I can figure it out.

[Sebastien Gouezel]

You can also do it using nat.rec_on. For instance, the proof of Baire theorem in docs#dense_Inter_of_open_nat does this.

[Heather Macbeth]

Interesting, I'll try it both ways!

[Sebastien Gouezel]

For another example, docs#hofer