coercion from Nat to ENat

Stream: mathlib4

[Yury G. Kudryashov]

It seems that we'll have to restate many WithTop lemmas for ENat because WithTop lemmas use WithTop.some and ENat uses Nat.cast.

[Yury G. Kudryashov]

In Lean 3, this didn't matter because these were defeq instances of has_coe_t but in Lean 4 these are different functions.

[Yury G. Kudryashov]

I'm adding a lemma some_eq_coe in !4#2186 (not pushed yet).

[Eric Wieser]

This seems like a pretty annoying problem, and it will come up again for:

• ennreal
• any future attempt to unrevert @Anne Baanen's refactor merging nat.cast and algebra_map

[Eric Wieser]

• lemmas about Int.ofNat in Std vs the same lemmas about Nat.cast in mathlib

[Chris Hughes]

I was hoping there weren't many WithTop lemmas. I added stuff like bot_add when I ported the file.

[Floris van Doorn]

Are these functions not definitionally equal anymore in Lean 4? Since docs4#NatCast is a class, can we just provide an instance that is definitionally the right function?

Or are they definitionally equal, but only after unfolding semireducible definitions (and in Lean 3 it was just unfolding instances)?

[Floris van Doorn]

@Eric Wieser

• We don't have a RealCast, so I don't know how this will come up for ENNReal.
• I don't see docs4#Int.ofNat. Do you mean docs4#OfNat vs docs4#NatCast ?

[Eric Wieser]

It's the later, they're definitionally equal but syntactically different

[Eric Wieser]

docs4#Int.ofNat not working is a docs bug, it's the constructor for docs4#Int

[Eric Wieser]

Maybe there's no coercion defined though

[Floris van Doorn]

Hopefully Std still formulates all user-facing lemmas about Int using NatCast, not Int.ofNat? That should mostly eliminate that problem, I think.

[Yury G. Kudryashov]

They are defeq but the function themselves are semireducible.

[Floris van Doorn]

I see, that indeed sounds inconvenient.

[Eric Wieser]

It would be straightforward to add a shim to restore Lean3 behavior by having a global coe function that provides all Coe instances in mathlib

[Eric Wieser]

But perhaps not a good idea

[Gabriel Ebner]

Yury G. Kudryashov said:

They are defeq but the function themselves are semireducible.

Should we just make Nat.cast and co. reducible then? I think we already had issues with nondefeq diamonds because one instance used Int.ofNat and the other Nat.cast

[Eric Wieser]

If foo is reducibly bar, does that means that rw lemma_about_foo can apply to bar?

[Gabriel Ebner]

I only propose to make def Nat.cast reducible. Nat.cast n and Int.ofNat still wouldn't be reducibly defeq with this change.

[Eric Wieser]

I don't understand the difference between those claims; are you suggesting Nat.cast would unfold reducibly to docs4#NatCast .natCast?

[Gabriel Ebner]

Yes!

[Eric Wieser]

Why would that make any difference?

[Eric Wieser]

Is it because NatCast.natCast has special instance/projection reducibility?

[Gabriel Ebner]

Because IIRC we use the .instances transparency to unify TC instances, which unfolds NatCast.natCast but doesn't unfold (the current, semireducible) Nat.cast.

[Gabriel Ebner]

NatCast.natCast is the projection btw.

[Eric Wieser]

I don't see how that would solve the problem in this thread, but I can't imagine it being a bad idea either.

[Thomas Murrills]

Aside, but as another example of this policy helping with diamonds:

if we made Nat.cast, Int.cast, and the incoming Rat.cast (std4#101) reducible, the basic OfScientific Rat instance wouldn’t need a “pointless” Rat.cast in the definition in order to be defeq at .instances transparency to the division-ring-based instance for OfScientific Rat. (defequality at this transparency is required for norm_num to work safely with it, as long as we want to avoid a LawfulOfScientific class)

[Thomas Murrills]

fwiw, I built mathlib4 on master locally with Nat.cast and Int.cast marked reducible in std4, and nothing seemed to break. (It would be good if someone else could confirm, though.) Is there any risk of the change slowing anything down?

[Yury G. Kudryashov]

See also https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebra.2EAlgebra.2EBasic for discussion about algebra_map as a coe.