Cannot infer {a b} from f a ≤ f b when f 1 ≤ f 0

Stream: new members

[attoknot]

Hi. For some reason lean cannot infer a and b in this case. Does anyone have more information on this behaviour?

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  intro h
  let f : ℝ → ℝ := fun x => 0
  have monof : Monotone f := fun _ _ _ => by rfl
  have h' : f 1 ≤ f 0 := le_refl _
  #check h monof h'         /- h monof h' : ?m.45 ≤ ?m.46 -/
  #check @h _ monof 1 _ h'  /- h monof h' : 1 ≤ ?m.47 -/
  #check @h _ monof 1 0 h'  /- h monof h' : 1 ≤ 0 -/

(this is from the "Mathematics in Lean" book)

[attoknot]

it works when f is opaque

[attoknot]

this makes sense. lean probably can't match f 0 := 0 against f ?. we can't always have nice things. though, it is annoying that annotating the return type isn't enough and I have to give a and b explicitly

[Bbbbbbbbba]

I guess it still works as long as you can match it to your goal?

import Mathlib

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  intro h
  let f : ℝ → ℝ := fun x => 0
  have monof : Monotone f := fun _ _ _ => by rfl
  have h' : f 1 ≤ f 0 := le_refl _
  suffices (1 : ℝ) ≤ 0 from by lia
  exact h monof h'

[Bbbbbbbbba]

Incidentally this is much easier with push_neg:

import Mathlib

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  push_neg
  exact ⟨fun x => 0, fun _ _ _ => by rfl, 1, 0, by rfl, Real.zero_lt_one⟩

[attoknot]

thanks. turns out it was my fault that return type annotations weren't working. it works if I do

  have : (1 : ℝ) ≤ 0 := h monof h'

instead of 1 ≤ 0. polymorphic literals do require time to get used to...