Meta.isDefEq failure

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Meta.isDefEq fails to deduce that two defeq terms are defeq, causing simp to fail.

Steps to Reproduce

No doubt this can be minimised more, but

section algebra_hierarchy_classes_to_comm_ring

class Zero (α : Type) where
  zero : α

class One (α : Type) where
  one : α

class Semiring (α : Type) extends Add α, Mul α, Zero α, One α

class CommSemiring (R : Type) extends Semiring R

class Ring (R : Type) extends Semiring R

class CommRing (R : Type) extends Ring R

end algebra_hierarchy_classes_to_comm_ring

section algebra_hierarchy_morphisms

class FunLike (F : Type) (α : outParam Type) (β : outParam <| α → Type) where
  coe : F → ∀ a : α, β a

instance (priority := 100) FunLike.insthasCoeToFun {F α : Type} {β : α → Type} [FunLike F α β] : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe

structure ZeroHom (M N : Type) [Zero M] [Zero N] where
  toFun : M → N

class ZeroHomClass (F : Type) (M N : outParam Type) [Zero M] [Zero N]
  extends FunLike F M fun _ => N where

structure OneHom (M : Type) (N : Type) [One M] [One N] where
  toFun : M → N

class OneHomClass (F : Type) (M N : outParam Type) [One M] [One N]
  extends FunLike F M fun _ => N where

structure AddHom (M : Type) (N : Type) [Add M] [Add N] where
  toFun : M → N

class AddHomClass (F : Type) (M N : outParam Type) [Add M] [Add N]
  extends FunLike F M fun _ => N where

structure MulHom (M : Type) (N : Type) [Mul M] [Mul N] where
  toFun : M → N

infixr:25 " →ₙ* " => MulHom

class MulHomClass (F : Type) (M N : outParam Type) [Mul M] [Mul N]
  extends FunLike F M fun _ => N where

structure AddMonoidHom (M : Type) (N : Type) [Add M] [Zero M] [Add N] [Zero N] extends
  ZeroHom M N, AddHom M N

infixr:25 " →+ " => AddMonoidHom

class AddMonoidHomClass (F : Type) (M N : outParam Type) [Add M] [Zero M] [Add N] [Zero N]
  extends AddHomClass F M N, ZeroHomClass F M N

structure MonoidHom (M : Type) (N : Type) [Mul M] [One M] [Mul N] [One N] extends
  OneHom M N, M →ₙ* N

infixr:25 " →* " => MonoidHom

class MonoidHomClass (F : Type) (M N : outParam Type) [Mul M] [One M] [Mul N] [One N]
  extends MulHomClass F M N, OneHomClass F M N

structure MonoidWithZeroHom (M : Type) (N : Type)
  [Mul M] [Zero M] [One M] [Mul N] [Zero N] [One N] extends ZeroHom M N, MonoidHom M N

infixr:25 " →*₀ " => MonoidWithZeroHom

structure NonUnitalRingHom (α β : Type) [Add α] [Zero α] [Mul α]
  [Add β] [Zero β] [Mul β] extends α →ₙ* β, α →+ β

class MonoidWithZeroHomClass (F : Type) (M N : outParam Type) [Mul M] [Zero M] [One M]
  [Mul N] [Zero N] [One N] extends MonoidHomClass F M N, ZeroHomClass F M N

infixr:25 " →ₙ+* " => NonUnitalRingHom

structure RingHom (α : Type) (β : Type) [Semiring α] [Semiring β] extends
  α →* β, α →+ β, α →ₙ+* β, α →*₀ β

infixr:25 " →+* " => RingHom

class RingHomClass (F : Type) (α β : outParam Type) [Semiring α]
  [Semiring β] extends MonoidHomClass F α β, AddMonoidHomClass F α β,
  MonoidWithZeroHomClass F α β

instance instRingHomClass (R S : Type) [Semiring R] [Semiring S] :
    RingHomClass (R →+* S) R S where
  coe f := f.toFun

-- this is needed to create the troublesome instance `Algebra.instid`
def RingHom.id (α : Type) [Semiring α] : α →+* α := by
  refine' { toFun := _root_.id.. }

end algebra_hierarchy_morphisms

section HSMul_stuff

class HSMul (α : Type) (β : Type) (γ : outParam Type) where
  hSMul : α → β → γ

class SMul (M : Type) (α : Type) where
  smul : M → α → α

infixr:73 " • " => HSMul.hSMul

instance instHSMul {α β : Type} [SMul α β] : HSMul α β β where
  hSMul := SMul.smul

-- note that the function `SMulZeroClass.toSMul` is what disrupts `simp` later
class SMulZeroClass (M A : Type) extends SMul M A where

class SMulWithZero (R M : Type) extends SMulZeroClass R M where

instance MulZeroClass.toSMulWithZero (R : Type) [Mul R] [Zero R] : SMulWithZero R R where
  smul := (· * ·)

end HSMul_stuff

section Algebra_stuff

class Algebra (R A : Type) [CommSemiring R] [Semiring A] extends SMul R A,
  R →+* A where

-- needed for troublesome `Algebra.instid`
def RingHom.toAlgebra' {R S : Type} [CommSemiring R] [Semiring S] (i : R →+* S)
    : Algebra R S where
  smul c x := i c * x
  toRingHom := i

-- needed for troublesome `Algebra.instid`
def RingHom.toAlgebra {R S : Type} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
  i.toAlgebra'

-- comment this out and the failing `simp` works
instance Algebra.instid (R : Type) [CommSemiring R] : Algebra R R :=
  (RingHom.id R).toAlgebra

end Algebra_stuff

namespace Pi_stuff

instance instSMul {I : Type} {f : I → Type} {M : Type} [∀ i, SMul M <| f i] : SMul M (∀ i : I, f i) :=
  ⟨fun s x => fun i => s • x i⟩

end Pi_stuff

section oliver_example

theorem Pi.smul_apply {I : Type} {f : I → Type} {β : Type} [∀ i, SMul β (f i)] (x : ∀ i, f i) (b : β) (i : I) : (b • x) i = b • (x i) :=
  rfl

instance (R : Type) [CommRing R] : CommSemiring R where

-- `foo` and `bar` are defeq
example {R : Type} [CommRing R] : True :=
  let foo := (Algebra.instid R).toSMul
  let bar : SMul R R := SMulZeroClass.toSMul
  have : foo = bar := rfl -- they are defeq
  trivial

-- this proof works fine
example {α R : Type} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  simp only [Pi.smul_apply]

-- the presence of `bar` breaks the proof
-- set_option trace.Meta.isDefEq true in
example {α R : Type} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
  --  have : Algebra.toSMul = bar := rfl
  --  have : (Algebra.instid R).toSMul = bar := rfl
  fail_if_success simp only [Pi.smul_apply]
  -- the isDefEq trace indicates a failure of isDefEq to prove
  -- that two defeq things are defeq
  sorry

-- The proof is fixed if we use `Ring` instead of `CommRing`.
example {α R : Type} [Ring R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
  simp only [Pi.smul_apply]

end oliver_example

The relevant part of the trace.Meta.isDefEq output is

[Meta.isDefEq] ❌ fun i ↦ Algebra.toSMul =?= fun i ↦ bar ▼
  [] ✅ α =?= α
  [] ❌ Algebra.toSMul =?= bar ▼
    [] ❌ Algebra.toSMul =?= SMulZeroClass.toSMul ▼
      [] ❌ (Algebra.instid R).1 =?= SMulWithZero.toSMulZeroClass.1 ▼
        [] ❌ (Algebra.instid R).1 =?= { smul := fun x x_1 ↦ x * x_1 } ▼
          [] ✅ SMul R R =?= SMul R R
          [] ❌ SMul.smul =?= fun x x_1 ↦ x * x_1 ▼
            [] ❌ fun x x_1 ↦ x * x_1 =?= fun a ↦ SMul.smul a ▼
              [] ✅ R =?= R
              [] ❌ fun x ↦ x✝ * x =?= SMul.smul x✝ ▼
                [] ❌ fun x ↦ x✝ * x =?= fun a ↦ SMul.smul x✝ a ▼
                  [] ✅ R =?= R
                  [] ❌ x✝¹ * x✝ =?= SMul.smul x✝¹ x✝ ▼
                    [] ❌ @HMul.hMul =?= @SMul.smul
                    [onFailure] ❌ x✝¹ * x✝ =?= SMul.smul x✝¹ x✝
                    [] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝ ▼
                      [] ❌ @Mul.mul =?= @SMul.smul
                      [onFailure] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝
                      [onFailure] ❌ Mul.mul x✝¹ x✝ =?= SMul.smul x✝¹ x✝
          [onFailure] ❌ (Algebra.instid R).1 =?= { smul := fun x x_1 ↦ x * x_1 }

and in particular the failure on line 3 [] ❌ Algebra.toSMul =?= bar ▼ is unexpected because the terms are defeq.

Expected behavior: [What you expect to happen]

I would not expect that randomly adding a term to the local context would break a simp proof.

Actual behavior: [What actually happens]

In the presence of bar, simp now makes no progress.

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

Lean (version 4.0.0-nightly-2023-08-19, commit 63d2bdd4908b, Release) on Ubuntu

Additional Information

There are workarounds, for example one can use simp only [Pi.smul_apply _]. But telling users to add _s everywhere is not an ideal solution.

[mattrobball]

It appears (to the untrained eye) that the transparency of (Algebra.instid R).1 has decreased relative to the runs in other contexts.

[ocfnash]

I think it's worth emphasising that a solution to this would be especially valuable because of the frequent situations where we use simp rather than simp only.

[Kha]

It appears (to the untrained eye) that the transparency of (Algebra.instid R).1 has decreased relative to the runs in other contexts.

Yes, simp only unfolds [reducible] definitions for performance reasons; it seems the workaround avoids even getting to that point for other reasons. Is there a mathlib policy about whether two instances should be defeq without unfolding standard defs?

[mattrobball]

Does rw behave differently?

[mattrobball]

Also, if you blindly make everything reducible, we get down to id c =?= c which fails.

[Kha]

Then you didn't literally make everything reducible because id isn't! If you replace it with fun x => x, it works.

[mattrobball]

Ha ha! Thanks.

I don't think it has been mentioned above explicitly (but was emphasized in the Zulip topic that birthed this) but rw in place of simp only succeeds both in closing the goal and checking that defeq by unfolding.

I thought reducibility for rw was also reducible so am a little confused.

[eric-wieser]

Is there a mathlib policy about whether two instances should be defeq without unfolding standard defs?

I think the answer is "essentially yes", in light of this library note.

[eric-wieser]

Which is to say,

-- needed for troublesome `Algebra.instid`
def RingHom.toAlgebra' {R S : Type} [CommSemiring R] [Semiring S] (i : R →+* S)
    : Algebra R S where
  smul c x := i c * x
  toRingHom := i

-- needed for troublesome `Algebra.instid`
def RingHom.toAlgebra {R S : Type} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
  i.toAlgebra'

are breaking this rule and should be @[reducible] (though I don't know if that's enough)

[eric-wieser]

It's not enough; to make the mwe fail to fail, you also have to change

-def RingHom.id (α : Type) [Semiring α] : α →+* α := { toFun := _root_.id .. }
+@[reducible] def RingHom.id (α : Type) [Semiring α] : α →+* α := { toFun := (·) .. }

which is not a change we want to make

[Kha]

Well that is problematic. Both simp and TC inference fundamentally depend on such typeclass diamonds being defeq under [reducible].

[eric-wieser]

@kbuzzard, do you have a Zulip thread in mind that motivated this MWE?

[ocfnash]

do you have a Zulip thread in mind that motivated this MWE?

@eric-wieser Yes, see this message. You can see an example of this in Mathlib here: you can replace simp [Pi.smul_apply (snf.a i)] with simp [Pi.smul_apply _] but if you write just simp (or even simp [Pi.smul_apply]) then the Pi.smul_apply does not fire.