MIL 1180

Stream: new members

[boris]

I have this context

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

proof exact h monof h' fails with

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

How do I fix it?

Here's the full thing

import data.real.basic

example :
  ¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b :=
begin
  intro h,
  let f := λ x : ℝ, (0 : ℝ),
  have monof : monotone f,
  { intros _ _ _, exact le_refl _  },
  have h' : f 1 ≤ f 0,
    from le_refl _,
  have : 1 ≤ 0,
    from h monof h',
end

[Riccardo Brasca]

Sorry this was probably wrong

[Riccardo Brasca]

Wait

[Moritz Doll]

import data.real.basic

example :
  ¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b :=
begin
  intro h,
  let f := λ x : ℝ, (0 : ℝ),
  have monof : monotone f,
  { intros _ _ _, exact le_refl _  },
  have h' : f 1 ≤ f 0,
    from le_refl _,
  have : (1 : ℝ) ≤ 0,
    from h monof h',
  sorry,
end

what Riccardo wrote. this works

[Riccardo Brasca]

I should stop trying to answer using only my phone :big_smile:

[Moritz Doll]

it was the correct answer, I would say you shouldn't

[Riccardo Brasca]

Even better!

[boris]

thank you!

[boris]

I see. Lean is so good at knowing what type things are, it's confusing when it doesn't

[Patrick Massot]

Boris, we are sorry that the error message is so unhelpful. When you see this kind of puzzling error message, there are two things to check: if you are trying to apply a lemma, you should carefully check the type class assumptions of the lemma (the assumptions written in square brackets), otherwise you need to check Lean understood what you meant by clicking on terms in the info view (assuming you are using VSCode). If your case, after stating the inequality, you can click on 0 and 1 in the infoview to see they are natural numbers.

[boris]

I didn't realise I could inspect the types in Infoview like that! That's really handy. Thanks for guiding me through it, very helpful.

[Patrick Massot]

Here is an example of the first case I mentioned above:

import data.real.basic

example {a : ℝ} (ha : a ≠ 0) : a*a⁻¹ = 1 :=
begin
  rw mul_inv_eq_one,
  -- rewrite tactic failed, did not find instance of the pattern in the
  -- target expression _ = 1
  sorry
end

#check @mul_inv_eq_one -- this is a lemma about (multiplicative) groups

#check @mul_inv_cancel -- this is the lemma we wanted

[Patrick Massot]

In that sample I try to invoke a lemma whose name is very promising and Lean seems blind when it declares it cannot match the target with the pattern _ = 1. But what Lean really means is it doesn't see the 1 of a group (for the multiplication operation), as you can see by reviewing the square-bracket argument of that lemma.