Troubles with coercion

Stream: new members

[Wojtek Wawrów]

I'm having a couple issues solving one of tutorial exercises. Here is the whole thing, but the most relevant two lines are the two just before end

lemma bdd_above_segment {f : ℝ → ℝ} {a b : ℝ} (hf : ∀ x ∈ Icc a b, continuous_at_pt f x) :
∃ M, ∀ x ∈ Icc a b, f x ≤ M :=
begin
  by_contradiction H,
  push_neg at H,
  have : ∀ (N : ℕ), ∃ (x : ℝ), x ∈ Icc a b ∧ (N : ℝ) < f x,
    intro N,
    exact H N,
  choose u hu using this,
  have bnd : ∀ (N : ℕ), u N ∈ Icc a b,
    intro n,
    exact (hu n).left,
  have clust := bolzano_weierstrass bnd,
  rcases clust with ⟨c,bc,hc⟩,
  specialize hf c bc,
  unfold cluster_point at hc,
  cases hc with φ hφ,

  have blah := seq_continuous_of_continuous hf hφ.right,
  have unblah : tendsto_infinity (f ∘ u ∘ φ),
    {apply squeeze_infinity seq_limit_id,
    intro n,
    specialize hu (φ n),
    have ineq := id_le_extraction hφ.left n,
    have ineq2 := hu.right,
    calc n ≤ φ n : ineq
    ... ≤ (f ∘ u ∘ φ) n : ineq2,},
  exact not_seq_limit_of_tendstoinfinity unblah c blah,
end

Firstly, I'm getting a type mismatch at the first ∘ in the second-to-last line. I suspect it is some coercion issue, however don't understand why this is the case - u has type ℕ → ℝ and f has type ℝ → ℝ, so I don't know why, of all places, it complains there.
Secondly, if I sorry that last have, then I am getting issues because types of some objects, starting with clust, involve (λ (N : ℕ), u N) which, I thought, would be the same as just u. I looked at the model solution of this exercise, and it seems to be structured differently so somehow the issue doesn't arise. Can we salvage the last line of my solution?

[Kevin Buzzard]

Hey Wojtek!

As you probably know by now, the naturals are not a subset of the reals in any real sense in Lean, there's a coercion. If you uncomment the set_option pp.coercions false line at the top of the tutorial file then you can see all the coercions indicated with arrows. In particular you can see that your goal is actually ↑n ≤ (f ∘ u ∘ φ) n so your calc proof is not quite right as it stands because it proves n <= something and you want to prove ↑n <= something. I don't know what they teach you in the tutorial but here's a way to finish that calculation:

    calc (n : ℝ) ≤ φ n : by assumption_mod_cast
    ... ≤ (f ∘ u ∘ φ) n : le_of_lt ineq2,},

[Alex J. Best]

I really don't know why turning coercions off is done in this file, nobody uses lean this way and I just spent 10 minutes confused what was going on here as well..

[Kevin Buzzard]

When I fix this, I see that the error you get on the last line is

type mismatch at application
  not_seq_limit_of_tendstoinfinity unblah c blah
term
  blah
has type
  seq_limit (f ∘ (λ (N : ℕ), u N) ∘ φ) (f c)
but is expected to have type
  seq_limit (f ∘ u ∘ φ) c

so this doesn't seem to be an issue with u and (lam N, u N), this seems to be that blah is a proof that something is tending to f c but Lean is expecting a proof that it tends to c. You can fix the last line by letting Lean figure out what things are tending to:

exact not_seq_limit_of_tendstoinfinity unblah _ blah,

[Wojtek Wawrów]

this seems to be that blah is a proof that something is tending to f c but Lean is expecting a proof that it tends to c

ah I see, that one is just my sloppiness then.

[Wojtek Wawrów]

As for the first part: I don't think the tutorial discusses coercion issues or anything of that sort at all, I'm only aware of it as it is mentioned in one of the challenge problems

[Kevin Buzzard]

You should learn to read the error messages. They can be quite intimidating at first but they often tell you what is going on.

[Wojtek Wawrów]

Yeah I'm working on that. I saw that it was telling me the types were different, but after seeing the lambda u difference I didn't look at the c vs f c

[Kevin Buzzard]

Wojtek Wawrów said:

As for the first part: I don't think the tutorial discusses coercion issues or anything of that sort at all, I'm only aware of it as it is mentioned in one of the challenge problems

So the issue is that calc is just some big syntactic sugar for basically applying transitivity of <= on some type. However Lean was failing to guess the type in your proof because your first <= was between naturals :-)

[Wojtek Wawrów]

Okay, so playing around with what you told me, here is my understanding of what the bits and bobs do, correct me if any of these are wrong:

1. Since keeping or leaving set_option pp.coercions false doesn't seem to change whether the proof works, I suppose it is merely "visual", to indicate where coercions happen.
2. The reason I was getting a type error is not because of a type mismatch between f and u, but between the type of φ n and f(...) which I was trying to compare using ≤.
3. assumption_mod_cast has found the n ≤ φ n lemma, has automatically transformed it into ↑n ≤ ↑(φ n), which then allowed me to use ineq2 to complete the proof.

[Alex J. Best]

Yes pp stands for pretty printer, by default lean displays when it inserts coercions with a little up arrow so you know that a function is being applied there.
That sounds right to me