Defining auxiliary sequences in tutorial

Stream: new members

[Carlo Cabrera]

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.

[Carlo Cabrera]

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.

[Rob Lewis]

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

[Rob Lewis]

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

[Carlo Cabrera]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Carlo Cabrera]

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.

[Rob Lewis]

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

[Carlo Cabrera]

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.

[Kevin Buzzard]

Why do you need to even define the sequences?

[Carlo Cabrera]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

You'll just end up with ten goals

[Kevin Buzzard]

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

[Carlo Cabrera]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

What is the type of the squeeze theorem?

[Kevin Buzzard]

Just fill in the first few inputs which have round brackets

[Kevin Buzzard]

And apply that

[Carlo Cabrera]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

And then you can refine it

[Carlo Cabrera]

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!

[Mario Carneiro]

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

[Mario Carneiro]

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

[Carlo Cabrera]

Mario Carneiro said:

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

Nice tip, thank you.