import breaks simp

Stream: general

[Damiano Testa]

Dear All,

in the code below, something in the combination of the files Algebra.Order.Monoid.WithTop and Data.Nat.Basic is incompatible with a simp lemma. Can I get simp to apply the simp-lemma docs#WithBot.unbot'_coe, with both imports?

Thanks!

import Mathlib.Order.WithBot
import Mathlib.Algebra.Order.Monoid.WithTop
import Mathlib.Data.Nat.Basic

-- works
example {a b : ℕ} : WithBot.unbot' a b = b := WithBot.unbot'_coe _ _

-- both fail, unless you comment at least one of the two imports
-- `Mathlib.Algebra.Order.Monoid.WithTop` or `Mathlib.Data.Nat.Basic`
example {a b : ℕ} : WithBot.unbot' a b = b := by simp only [WithBot.unbot'_coe]
example {a b : ℕ} : WithBot.unbot' a b = b := by simp

[Yury G. Kudryashov]

I guess, Lean uses Nat.cast for coercion, not WithBot.some.

[Yury G. Kudryashov]

So, you need to either use docs#Nat.cast_withBot, or add a duplicate lemma that uses Nat.cast.

[Damiano Testa]

Ah, this indeed works with both imports:

example {a b : ℕ} : WithBot.unbot' a (WithBot.some b) = b := by simp only [WithBot.unbot'_coe]

[Damiano Testa]

It also highlights this porting note:

-- Porting note: changed this from `CoeTC` to `Coe` but I am not 100% confident that's correct.
instance coe : Coe α (WithBot α) :=
  ⟨some⟩

[Yury G. Kudryashov]

Anyway, we'll have this problem one way or another: if Lean usesNat.cast (like now), then you can't apply lemmas about WithBot.some, otherwise you can't apply lemmas about Nat.cast.

[Damiano Testa]

So, to try to understand, with the combination of those files, Lean produces a Nat.cast to WithBot Nat, but the two files separately do not suffice for the Nat.cast. Once the Nat.cast is available, Lean uses Nat.cast instead of WithBot.coe for the coercion.

Is this correct?

[Yury G. Kudryashov]

Yes, once you have an AddMonoidWithOne instance on WithBot Nat, it uses NatCast.

[Damiano Testa]

Would adding this lemma be reasonable?

@[simp]
theorem preferWithBotSomeToNatCast {a : ℕ} : Nat.cast a = WithBot.some a := rfl

[Yury G. Kudryashov]

This is exactly src#Nat.cast_withBot

[Damiano Testa]

Ah, it is simply not simp!

[Yury G. Kudryashov]

But if you make it a simp lemma, one can be surprised about lemmas about Nat.cast not working.

[Damiano Testa]

Ok, I'll see if I can simply add it to the simp call and be done with it.

[Damiano Testa]

(This is within some meta-programming, so I may report back with more questions!)

[Damiano Testa]

Anyway, thank you very much: now the issue is perfectly clear!

[Yury G. Kudryashov]

In Lean 3, this was not an issue because both functions were hidden behind coe but Lean 4 unfolds coercions.

[Yury G. Kudryashov]

On the one hand, we no longer need to worry about some diamonds. OTOH, we get these problems.

[Damiano Testa]

Ok, this example clarified a little for me the issue with coercions in Lean4: this has been super helpful, thanks again!