Problem with function application

Stream: new members

[Emiel Lanckriet]

I'm going through Mathematics in Lean and I came across an exercise where the environment is

h : ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b : ℝ}, f a ≤ f b → a ≤ b,
f : ℝ → ℝ := λ (x : ℝ), 0,
monof : monotone f,
h' : f 1 ≤ f 0
⊢ false

and I want to make a term of the form 1 \leq 0 as follows
have h1 : 1 ≤ 0 := h monof h'.
However, I get the following error:

invalid type ascription, term has type
  ?m_1 ≤ ?m_2
but is expected to have type
  1 ≤ 0

I don't really understand, why I don't get 1 ≤ 0.

[Kevin Buzzard]

I doubt your 1 is the 1 you want. If you don't say (1 : \R) then it defaults to nat. The error means "I'm looking for two real numbers but all I see is naturals"

[Emiel Lanckriet]

Thanks, indeed, declaring that I want 1 and 0 to be reals does the trick. Is there anything in the error message that hints that this was the problem?

[Scott Morrison]

You could probably turn on set_option pp.all true (or some intermediate pretty printer setings, e.g. pp.notation false + pp.implicits true.

[Scott Morrison]

That would show you what type the le was in.

[Emiel Lanckriet]

Thanks, it makes the errors to complicated to turn on all the time, but it could help when digging deeper.

[Kevin Buzzard]

I just know that when the user types 1 it means the natural 1 unless specified otherwise. It's an issue which comes up all the time on this chat

[Kevin Buzzard]

There's even an issue about it on the natural number game. To fix it you need to hack core lean

[Reid Barton]

Usually Lean tries to expand whatever part of the expressions don't agree in an error like this--if the two expressions still appear to agree (e.g. here it looks like we could set ?m_1 = 1 and ?m_2 = 0) then usually the reason is that the types are wrong or there is a type class or universe issue.

[Reid Barton]

I wonder whether it would be sensible for have h : T := e to use e to elaborate T, like def does