coercion issue in NumberTheory.LegendreSymbol.MulCharacter

Stream: mathlib4

[Kevin Buzzard]

Teaching is finally over, and I was looking at the state of the mathlib4 PRs. mathlib4#2994 NumberTheory.LegendreSymbol.MulCharacter caught my eye, it's not compiling right now. Here's an issue (on master, not on that branch):

import Mathlib.Algebra.CharP.Basic
import Mathlib.Algebra.EuclideanDomain.Instances
import Mathlib.Algebra.Group.ConjFinite

-- The domain of our multiplicative characters
variable (R : Type u) [CommMonoid R]

-- The target
variable (R' : Type v) [CommMonoidWithZero R']

/-- Define a structure for multiplicative characters.
A multiplicative character from a commutative monoid `R` to a commutative monoid with zero `R'`
is a homomorphism of (multiplicative) monoids that sends non-units to zero. -/
structure MulChar extends MonoidHom R R' where
  map_nonunit' : ∀ a : R, ¬IsUnit a → toFun a = 0

variable {R R'}

instance coeToFun : CoeFun (MulChar R R') fun _ => R → R' :=
  ⟨fun χ => χ.toFun⟩

-- evil
@[simp]
theorem coe_coe (χ : MulChar R R') : (χ.toMonoidHom : R → R') = χ :=
  rfl

set_option maxHeartbeats 2000 in
set_option trace.Debug.Meta.Tactic.simp true in
example {R : Type u} [CommMonoidWithZero R] (χ : MulChar R R') (a : R) :
  χ a = (0 : R') := by
  -- `⊢ OneHom.toFun (↑χ.toMonoidHom) a = 0`
  -- Remark: in Lean 3 the goal is `⇑χ a = 0`
  dsimp -- loops
/-
...
[Debug.Meta.Tactic.simp] rewrite result ↑χ.toMonoidHom a => OneHom.toFun (↑χ.toMonoidHom) a

[Debug.Meta.Tactic.simp] no theorems found for pre-rewriting OneHom.toFun (↑χ.toMonoidHom) a

[Debug.Meta.Tactic.simp] rewrite result OneHom.toFun (↑χ.toMonoidHom) a => ↑↑χ.toMonoidHom a

[Debug.Meta.Tactic.simp] no theorems found for pre-rewriting ↑↑χ.toMonoidHom a

[Debug.Meta.Tactic.simp] rewrite result ↑↑χ.toMonoidHom a => ↑χ.toMonoidHom a

[Debug.Meta.Tactic.simp] no theorems found for pre-rewriting ↑χ.toMonoidHom a

[Debug.Meta.Tactic.simp] rewrite result ↑χ.toMonoidHom a => OneHom.toFun (↑χ.toMonoidHom) a

[Debug.Meta.Tactic.simp] no theorems found for pre-rewriting OneHom.toFun (↑χ.toMonoidHom) a

[Debug.Meta.Tactic.simp] rewrite result OneHom.toFun (↑χ.toMonoidHom) a => ↑↑χ.toMonoidHom a

[Debug.Meta.Tactic.simp] no theorems found for pre-rewriting ↑↑χ.toMonoidHom a

[Debug.Meta.Tactic.simp] rewrite result ↑↑χ.toMonoidHom a => ↑χ.toMonoidHom a

[Debug.Meta.Tactic.simp] no theorems found for pre-rewriting ↑χ.toMonoidHom a

[Debug.Meta.Tactic.simp] rewrite result ↑χ.toMonoidHom a => OneHom.toFun (↑χ.toMonoidHom) a

...
-/

I feel like coercions have changed a lot but now people understand the lean 4 versions. Seems to me that coe_coe is evil (it makes the linter time out and I think it's causing the loop). Two questions then: (1) why is the goal so much more ugly in mathlib4 than mathlib3 and (2) what is the recommended fix for this? The code above is just cherrypicked from the autoported NumberTheory.LegendreSymbol.MulCharacter other than the looping example (this showed up when trying to debug some errors in the file). Perhaps a better question is (3) is there now some place where we can read about Lean 4 coercions, how they've changed, and how I'm supposed to immediately spot that coe_coe is for some reason a bad lemma (I still don't really understand why) without having the timing out linter tell me this?

[Eric Wieser]

It sounds like there are a bunch of lemmas like the ones in !4#3035 which need re-adding

[Eric Wieser]

We lost a lot of coercion lemmas due to mistakes early in the port that we only worked out how to correct later

[Eric Wieser]

instance coeToFun : CoeFun (MulChar R R') fun _ => R → R' :=
  ⟨fun χ => χ.toFun⟩

is an evil instance

[Eric Wieser]

The better spelling is

instance funLike : FunLike (MulChar R R') R (fun _ => R') :=
  ⟨fun χ => χ.toFun⟩

[Eric Wieser]

Bu t the best thing to do is first backport a monoid_hom_class instance to mathlib3

[Eric Wieser]

(port-status#number_theory/legendre_symbol/mul_character for reference)

[Joël Riou]

Is CoeFun evil in general? For example, in CategoryTheory.ConcreteCategory.Basic, we have a CoeFun definition which is used in Algebra/Category/MonCat/Basic.lean (and some other PR). Should we replace all these by FunLike?

[Eric Wieser]

CoeFun is almost always the wrong choice for algebra. I can't really say for category theory

[Eric Wieser]

In general if you extend something that uses CoeFun then you should also use CoeFun

[Kevin Buzzard]

@Jeremy Tan do you want to do the backport?

[Kevin Buzzard]

Will this fix the issue with the ugly prettyprinter output in lean 4 or is that something else?

[Eric Wieser]

Yes, it will fix that too

[Jeremy Tan]

Kevin Buzzard said:

Jeremy Tan do you want to do the backport?

Ehh, I could try

[Jeremy Tan]

I haven't touched Lean 3 and mathlib3 yet, so what exactly needs to be done?

[Kevin Buzzard]

Oh it's OK, I can do it now. I just conjectured you'd do it more quickly but I have some time right now.

[Kevin Buzzard]

Eric Wieser said:

Bu t the best thing to do is first backport a monoid_hom_class instance to mathlib3

Wait -- it's there already right? So is the next thing to delete coeToFun in the mathlib4 version?

[Eric Wieser]

instance : mul_char_class needs to move up the file

[Eric Wieser]

But doesn't need backporting

[Xavier Roblot]

I am reviving this thread since I am working on the port of NumberTheory.LegendreSymbol.GaussSum. Some of the difficulties I have seem to be related to the issues discussed in this thread and it seems that the solutions discussed here have not been yet implemented. Is this correct?

[Kevin Buzzard]

I certainly don't ever remember doing the thing I claimed I would do above.

[Xavier Roblot]

All right, so I think I'll try to incorporate the changes suggested above to MulChar in this PR and submit everything together for review.