naming: `map_int_cast` vs `map_natCast` vs `map_ratCast`

Stream: mathlib4

[Moritz Firsching]

Just when I thought I had somewhat understood the naming conventions, I stumbled upon these three names:

map_int_cast
map_natCast
map_ratCast

Is this an oversight, or is there a deeper reason why they are not consistent?

[Chris Hughes]

Oversight

[Moritz Firsching]

ok, I will prepare a fix renaming map_int_cast to map_intCast and similar

[Moritz Firsching]

mathlib4#1337

[Heather Macbeth]

Given that

import Mathlib.Data.Nat.Cast.Basic

example [Ring α] [Ring β] [RingHomClass F α β] (f : F) : f 2 = 2 :=
  map_natCast f 2

works and map_natCast is tagged simp, why doesn't

import Mathlib.Data.Nat.Cast.Basic

example [Ring α] [Ring β] [RingHomClass F α β] (f : F) : f 2 = 2 := by
  simp

work?

[Heather Macbeth]

(Encountered while debugging something previously proved with map_bit0.)

[Scott Morrison]

The head of the expression is a variable, so there is nothing to index this on. This is the same behaviour as in Lean 3.

[Heather Macbeth]

Interesting, should we remove the simp tag then?

[Heather Macbeth]

And would it be worth adding simp-lemmas for some small numbers,

lemma map_two [Ring α] [Ring β] [RingHomClass F α β] (f : F) : f 2 = 2 :=
  map_natCast f 2

lemma map_three [Ring α] [Ring β] [RingHomClass F α β] (f : F) : f 3 = 3 :=
  map_natCast f 3

[Scott Morrison]

They aren't going to work any better with simp, so I'm not sure where we'd be using them.

[Heather Macbeth]

Oh ... the problem is RingHomClass, not Nat.cast?

[Reid Barton]

Is the head really a variable? Maybe this is https://github.com/leanprover/lean4/issues/1937 instead?

[Kevin Buzzard]

Which apparently has been fixed :-)

[Reid Barton]

Yes but I don't know if mathlib4 is on the new version yet.

[Eric Wieser]

The head symbol here is FunLike.coe

[Scott Morrison]

mathlib4#1397 bumps to the latest nightly, which should bring in the fix for lean4#1937.

[Scott Morrison]

(anagram not intended...?)

[Eric Wieser]

That link doesn't work for me?