Coercion of 1 : ℕ+ to 1 : ℝ≥0∞

Stream: general

[Strategist _]

Hi, I noticed something weird about Lp spaces.

If I run the code

import Init.Data.Nat.Basic
import Mathlib
import Mathlib.Data.ENNReal.Basic
import Mathlib.MeasureTheory.Function.LpSpace

open MeasureTheory
open ENNReal

variable (f : Lp ℝ ((1 : ℕ+) : ℝ≥0∞) (volume : Measure (Fin 1 → ℝ)))
#check (f : Lp ℝ 1 (volume : Measure (Fin 1 → ℝ)))

I get the error

type mismatch
  f
has type
  ↥(Lp ℝ (↑↑1) volume) : Type
but is expected to have type
  ↥(Lp ℝ 1 volume) : Type

I think this is happening because for some reason ((1 : ℕ+) : ℝ≥0∞) and (1 : ℝ≥0∞) are not definitionally equal, which they need to be in the argument of Lp?

Does anyone know any way to circumvent this or get Lean to recognize that those are the same thing?

[Ruben Van de Velde]

What's weird about it?

[Strategist _]

I would expect the coercion of 1 from ℕ+ to ℝ≥0∞ to behave the same way as just 1 in ℝ≥0∞ since they should in principle be the same thing. Is there some way to get Lean to interpret it that way?

[Yury G. Kudryashov]

Is ((1 : PNat) : ENNReal) = 1 a rfl?

[Yury G. Kudryashov]

BTW, you need a newline after the first ``` to get syntax highlighting.

[Yury G. Kudryashov]

Found it: docs#Real.instOne uses an irreducible private def Real.one.

[Yury G. Kudryashov]

You can move NatCast instance earlier, then redefine One Real using one := (1 : Nat), similarly for Zero Real.

[Yury G. Kudryashov]

This will make Nat.cast 1 = 1 a rfl for Reals.

[Eric Wieser]

Or we just change Real.one to not be irreducible, since docs#Real.instNatCast is

[Eric Wieser]

Probably we have the same problem with Real.zero

[Eric Wieser]

How much performance do we lose if we drop all the irreducible_s in that file?

[Yury G. Kudryashov]

AFAIR, Lean used to unfold Real-related semireducible definitions during hard-to-unify apply, convert etc.

[Strategist _]

So just to clarify, you'd recommend modifying my local copy of Mathlib to get that to be a rfl?

[Kevin Buzzard]

If you modify your local mathlib then your code can't be used by anyone else. You could make a WIP PR removing all the irreducibles in that file and then benchmark it to see what happens.

[Yury G. Kudryashov]

There are 2 ways you can deal with this issue:

• make ((1 : Nat) : Real) = 1 a rfl;
• define Lp.cast (h : p = q) as a continuous linear equivalence between Lp with p and Lp with q (hint: reuse Equiv.subtypeEquivRight for the equivalence), then apply it explicitly to get from 1 term to another; pros and cons compared to the "make it rfl" approach:
  • pros:
    • it works even if rfl breaks again;
    • you don't have to recompile half of Mathlib.
  • cons: it needs explicit Lp.casts here and there.

With each approach, you have 2 ways to deal with your additions/modifications to the library:

• modify your local copy of Mathlib and use it; pros and cons compared to the next one:
  • pros: no need to go through the review process;
  • cons:
    • if you ever want to upgrade Mathlib, then you'll have to merge the changes;
    • you don't get precompiled oleans from lake exe cache (if you go with "make it rfl");
• open a PR with your modifications.