simp regression with MonoidHomClass

Stream: mathlib4

[Floris van Doorn]

I noticed a regression with simp below:

import Mathlib.Algebra.Hom.Group

-- this works:
theorem map_one' [MulOneClass M] [MulOneClass N] [MonoidHomClass F M N] (f : F) : f 1 = 1 :=
  by simp [map_one f]

-- neither of these work. The corresponding version in Lean 3 works
theorem map_one' [MulOneClass M] [MulOneClass N] [MonoidHomClass F M N] (f : F) : f 1 = 1 :=
  by simp [map_one]
  -- by simp

Note that the left-hand side of the current goal is
@FunLike.coe F M (fun a ↦ (fun x ↦ N) a) MulHomClass.toFunLike f 1 : (fun x ↦ N) 1 and that of the simp lemma is
@FunLike.coe F M (fun a ↦ (fun x ↦ N) a) OneHomClass.toFunLike f 1 : (fun x ↦ N) 1
These are definitionally equal by unfolding instances.

[Kevin Buzzard]

Is this related to https://github.com/leanprover/lean4/issues/1937 ?

[Kevin Buzzard]

theorem map_one'' [MulOneClass M] [MulOneClass N] [MonoidHomClass F M N] (f : F) : f 1 = 1 :=
  by rw [map_one] -- works

[Gabriel Ebner]

Uggh, this is fallout from https://github.com/leanprover/lean4/commit/1cc58e60eff14514fa2132df018827828ef7e826

[Gabriel Ebner]

Small repro:

class FunLike (F : Type _) (A : outParam (Type _)) (B : outParam (A → Type _)) where toFun : F → ∀ a, B a
instance [FunLike F A B] : CoeFun F fun _ => ∀ a, B a where coe := FunLike.toFun
class One (M) where one : M
instance [One M] : OfNat M (nat_lit 1) where ofNat := One.one
class OneHomClass (F) (A B : outParam _) [One A] [One B] extends FunLike F A fun _ => B
class MulHomClass (F) (A B : outParam _) [Mul A] [Mul B] extends FunLike F A fun _ => B
class Monoid (M) extends Mul M, One M
class MonoidHomClass (F) (A B : outParam _) [Monoid A] [Monoid B] extends MulHomClass F A B, OneHomClass F A B

theorem map_one [Monoid A] [Monoid B] [OneHomClass F A B] (f : F) : f 1 = 1 := sorry
example [Monoid M] [Monoid N] [MonoidHomClass F M N] (f : F) : f 1 = 1 := by
  simp only [map_one]

[Floris van Doorn]

Are you saying this is a universe metavariable issue? That simp fails because it has to assign universe metavariables?

[Kevin Buzzard]

class FunLike (F : Type) (A : outParam (Type)) (B : outParam (A → Type)) where toFun : F → ∀ a, B a
instance [FunLike F A B] : CoeFun F fun _ => ∀ a, B a where coe := FunLike.toFun
class One (M) where one : M
instance [One M] : OfNat M (nat_lit 1) where ofNat := One.one
class OneHomClass (F) (A B : outParam _) [One A] [One B] extends FunLike F A fun _ => B
class MulHomClass (F) (A B : outParam _) [Mul A] [Mul B] extends FunLike F A fun _ => B
class Monoid (M) extends Mul M, One M
class MonoidHomClass (F) (A B : outParam _) [Monoid A] [Monoid B] extends MulHomClass F A B, OneHomClass F A B

theorem map_one [Monoid A] [Monoid B] [OneHomClass F A B] (f : F) : f 1 = 1 := sorry
example [Monoid M] [Monoid N] [MonoidHomClass F M N] (f : F) : f 1 = 1 := by
  simp only [map_one]

(change all Type _ to Type) makes the error go away.

[Gabriel Ebner]

Are you saying this is a universe metavariable issue? That simp fails because it has to assign universe metavariables?

Yes, see lean4#1951, lean4#1952, lean4#1953

[Kevin Buzzard]

Does this also happen to fix lean4#1937 ?

[Gabriel Ebner]

I think that's a completely different issue.

[Kevin Buzzard]

I only asked because it was also simp not rewriting when it looked like it should.