Zulip Chat Archive

Stream: new members

Topic: Recursively defined sequence within proof


view this post on Zulip Heather Macbeth (Oct 19 2020 at 20:54):

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.

view this post on Zulip Floris van Doorn (Oct 19 2020 at 20:58):

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)

view this post on Zulip Floris van Doorn (Oct 19 2020 at 20:59):

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

view this post on Zulip Floris van Doorn (Oct 19 2020 at 21:00):

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

view this post on Zulip Heather Macbeth (Oct 19 2020 at 21:00):

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?

view this post on Zulip Floris van Doorn (Oct 19 2020 at 21:03):

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.

view this post on Zulip Heather Macbeth (Oct 19 2020 at 21:04):

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

view this post on Zulip Sebastien Gouezel (Oct 19 2020 at 21:08):

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.

view this post on Zulip Heather Macbeth (Oct 19 2020 at 21:10):

Interesting, I'll try it both ways!

view this post on Zulip Sebastien Gouezel (Oct 19 2020 at 21:13):

For another example, docs#hofer


Last updated: May 15 2021 at 22:14 UTC