Algebra.cast and algebraMap

Stream: mathlib4

[Daniel Weber]

Currently something which is quite annoying for automation is that simp fails to show algebraMap A B a = (a : B):

import Mathlib

open algebraMap

example (A B : Type*) [CommSemiring A] [Semiring B] [Algebra A B] (a : A) : algebraMap A B a = a := by
  fail_if_success simp
  rfl

What's the best way to solve this? It's possible to just add it as a @[simp] lemma (probability scoped to algebraMap), and I've also thought about making Algebra.cast reducible, but I'm not sure about the exact pros and cons of either

[Kevin Buzzard]

I have been working with algebraMap with algebraMap open and am also a bit confused about what the simp normal form is supposed to be. For quotients $R/I$ there's another coercion from $R$ which exists even without algebraMap open (I asked a question about this recently) (edit: here)

[Eric Wieser]

We have two spellings here because the port interrupted a major refactor by @Anne Baanen. I think changes to coercions to lean 4 made the original plan untenable.

[Eric Wieser]

My vote would be to drop Algebra.cast until someone finds time to come up with a plan for a replacement refactor.

[Kevin Buzzard]

So you're saying "drop the coercion associated to [Algebra A B]"? I'm using this coercion a lot, I love it.

[Eric Wieser]

Or make it mean algebraMap

[Kevin Buzzard]

My understanding was that Lean 4 does not allow us to have things like algebraMap (whose type is not a function type) as coercions? I thought that this was why we introduced Algebra.cast in the first place?

[Eric Wieser]

Arguably they work fine, and it's just the pretty-printing that doesn't

[Eric Wieser]

I think the original goal might have been to drop Nat.cast and Int.cast and Rat.cast and use Algebra.cast as the spelling of all of them

[Yaël Dillies]

That goes against making Nat/Int/Rat foundational, right?

[Eric Wieser]

I don't think so?

[Eric Wieser]

It goes against the "every coercion should be a different function" thing that core seems to have designed for, but so does the design of Dfunlike

[Eric Wieser]

A data only AlgebraCast type class next to docs#NatCast would do the trick.

[Daniel Weber]

I've been experimenting with making Algebra.cast @[reducible] on branch#CommandMaster_castReducible (#14601)