failed to synthesize implicits in example from MIL ch3.3

Stream: new members

[Rado Kirov]

In chapter 3.3, I can only get the following solution to work by unwrapping the implicit arguments:

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  intro h
  let f := fun x : ℝ ↦ (0 : ℝ)
  have monof : Monotone f := by
    intro a b h
    norm_num
  have h' : f 1 ≤ f 0 := le_refl _
  have h'' := @h f monof  -- why not h monof
  have ff := @h'' 1 0 h' -- why not h'' h'
  linarith

[Chris Wong]

Is it because, when you specify monof, it tries to skip ahead and fill in a and b too?

[Chris Wong]

It might work if you mark a b as strict implicit parameters
https://lean-lang.org/doc/reference/latest//Terms/Functions/#implicit-functions

[Ruben Van de Velde]

Yeah, though that still doesn't help when you continue:

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 := by
    intro a b h
    norm_num
  have h' : f 1 ≤ f 0 := le_refl _
  have : (0 : ℝ) ≤ 1 := h monof h' -- works
  have := h monof h'
    -- failed to infer 'have' declaration type;
    -- don't know how to synthesize implicit argument 'b'
    -- don't know how to synthesize implicit argument 'a'

which goes against my intuition

[Rado Kirov]

Great point about strict implicits, but indeed only gets rid of the first mystery. For the second, to add to the confusion, if I extract it all into a separate example, it works

def zero_fn := fun _ : ℝ ↦ (0 : ℝ)
example (h: ∀ {{a b}}, zero_fn a ≤ zero_fn b → a ≤ b) : a ≤ b := by
  have h' : zero_fn 1 ≤ zero_fn 0 := le_refl _
  exact h h'

so something in the bigger proof context makes it not work?

[Chris Wong]

If we change to let f := fun x : ℝ ↦ x - x then it works.

I suspect the problem is that Lean unfolds f prematurely to the constant 0, which is independent of the argument.