Zulip Chat Archive

Stream: new members

Topic: Defining auxiliary sequences in tutorial


view this post on Zulip Carlo Cabrera (May 17 2020 at 21:14):

I'm working through the tutorials, and one part has me wanting to try to figure out how to apply the squeeze theorem to show that a sequence has a certain limit. See the following example.

example (x : ) (u :   ) (h :  n, u n  x) (h' :  n : , x - 1 /(n+1)  u n) :
(seq_limit u x) :=
begin
  let v :    := λ n, x,
  have seq_v :  n : , v n = x,
    intro n,
    linarith,
  let w :    := λ n, x - 1 / (n + 1),
  have seq_w :  n : , w n = x - 1 / (n + 1),
    sorry,
  sorry
end

I have the sequence u, and it is sandwiched between two other convergent sequences. However, I need to define these two other sequences, and the way I'm doing it now doesn't seem to be the right way. In particular, the way I've defined v seems to not be too transparent for Lean, though I've managed to convince it that it has the property that I need. Unfortunately, what I did for v doesn't work for w.

Can anyone point me in the right direction? Thank you.

view this post on Zulip Carlo Cabrera (May 17 2020 at 21:22):

I guess I should be using choose here? That seems to be how one of the exercises constructed a sequence, but my hypotheses don't seem to have the right form for choose.

view this post on Zulip Rob Lewis (May 17 2020 at 21:27):

When you're looking for help here it's best to post a #mwe so that people can try out your code.

view this post on Zulip Rob Lewis (May 17 2020 at 21:28):

But I can see this one: seq_v and seq_w are true by definition. You can prove both of these with intro, refl.

view this post on Zulip Carlo Cabrera (May 17 2020 at 21:34):

Rob Lewis said:

But I can see this one: seq_v and seq_w are true by definition. You can prove both of these with intro, refl.

I thought that was an #mwe! In any case, you're right. It does work. I could swear I tried refl first, because I knew it was true by definition, but it seems I had not. Thanks for taking the time to address my silly question.

view this post on Zulip Kevin Buzzard (May 17 2020 at 21:34):

A mwe will run for me if I just cut and paste what you posted. This doesn't.

view this post on Zulip Kevin Buzzard (May 17 2020 at 21:35):

Oh! Maybe set v : ℕ → ℝ := λ n, x with seq_v might do everything for you in one go.

view this post on Zulip Carlo Cabrera (May 17 2020 at 21:37):

Kevin Buzzard said:

A mwe will run for me if I just cut and paste what you posted. This doesn't.

Yes, it does rely on the definition of seq_limit in the tutorial. Thought that was fine. Sorry about that! I have not yet managed to track down the definition of the limit of a sequence in mathlib.

view this post on Zulip Rob Lewis (May 17 2020 at 21:37):

Kevin Buzzard said:

Oh! Maybe set v : ℕ → ℝ := λ n, x with seq_v might do everything for you in one go.

Not quite, it will give you the unapplied version v = lambda n, ... instead of forall n, v n = ...

view this post on Zulip Carlo Cabrera (May 17 2020 at 21:55):

Edit: Fixed now.

Here is the #mwe.

import data.real.basic

def seq_limit (u :   ) (l : ) : Prop :=  ε > 0,  N,  n  , abs (u n - l)  ε

example (x : ) (u :   ) (h :  n, u n  x) (h' :  n : , x - 1 /(n+1)  u n) :
(seq_limit u x) :=
begin
  let v :    := λ n, x,
  have seq_v :  n : , v n = x := by intro; refl,
  let w :    := λ n, x - 1 / (n + 1),
  have seq_w :  n : , w n = x - 1 / (n + 1) := by intro; refl,
  admit
end

I feel like there should be a better way to define the auxiliary sequences I need, but I suppose proceeding with the example as written will work.

view this post on Zulip Kevin Buzzard (May 17 2020 at 21:59):

Why do you need to even define the sequences?

view this post on Zulip Carlo Cabrera (May 17 2020 at 22:04):

I would like to use the squeeze theorem (defined earlier in the tutorial) to conclude. I don't need the squeeze theorem to finish the proof; I was just thinking it would be good to know how to use it. (I know I don't state the squeeze theorem in the example, but I don't think that's necessary for the question. I can include the statement if it's needed.)

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:06):

Why not just apply the squeeze theorem and then deal with all the inputs later?

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:07):

If a function needs ten inputs and then spits out a proof of theorem X, and your goal is theorem X then you can just apply the function anyway

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:07):

You'll just end up with ten goals

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:08):

It's this weird backwards way that computer scientists think about proofs

view this post on Zulip Carlo Cabrera (May 17 2020 at 22:12):

Good question. Part of the reason is that I don't even understand the tactic state after applying the squeeze theorem. These ?m_1s show up in the goals of my tactic state. I think those ?m_1s are meant to be the sequences I wanted to define.

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:13):

Maybe you should apply it and just fill in some of the easy inputs

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:13):

What is the type of the squeeze theorem?

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:14):

Just fill in the first few inputs which have round brackets

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:14):

And apply that

view this post on Zulip Carlo Cabrera (May 17 2020 at 22:16):

Here is the type, which is what I get when I #check squeeze. (That's what you meant, right?)

squeeze :
  seq_limit ?M_1 ?M_4 
  seq_limit ?M_3 ?M_4 
  ( (n : ), ?M_1 n  ?M_2 n)  ( (n : ), ?M_2 n  ?M_3 n)  seq_limit ?M_2 ?M_4

Sadly the first few inputs seem to require furnishing the sequences I wanted to define.

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:18):

Why not skip the first two inputs by putting underscores and then fill in the next two with h and h'

view this post on Zulip Kevin Buzzard (May 17 2020 at 22:18):

And then you can refine it

view this post on Zulip Carlo Cabrera (May 17 2020 at 22:19):

Kevin Buzzard said:

Why not skip the first two inputs by putting underscores and then fill in the next two with h and h'

Yup, I realised that just after sending my last message. :) That also works. Thank you!

view this post on Zulip Mario Carneiro (May 17 2020 at 22:19):

You can also #check @squeeze so that it doesn't do the metavariable thing

view this post on Zulip Mario Carneiro (May 17 2020 at 22:19):

and supply the appropriate construction with @squeeze _ _ (my sequence) _ _ _ _ _

view this post on Zulip Carlo Cabrera (May 17 2020 at 22:22):

Mario Carneiro said:

You can also #check @squeeze so that it doesn't do the metavariable thing

Nice tip, thank you.


Last updated: May 09 2021 at 19:11 UTC