class IsCommutative (op : α → α → α) where
comm : op x y = op y x
class LeftUnit (α : Type u) extends Mul α
class Monoid (α : Type u) extends LeftUnit α
class CommMonoid (α : Type u) extends LeftUnit α where
mul_comm {x y : α} : x * y = y * x
instance [CommMonoid α] : IsCommutative (α := α) (· * ·) where
comm := CommMonoid.mul_comm
instance [CommMonoid α] : Monoid α where
theorem foo [Monoid α] [IsCommutative (α := α) (· * ·)] {x y : α} :
x * y = z ↔ y * x = z := by
rw [IsCommutative.comm (op := (· * ·))]
exact Iff.rfl
instance : CommMonoid Nat where
mul_comm := Nat.mul_comm _ _
set_option trace.Meta.synthInstance true
variable (a b c : Nat) (h : a * b = c)
#check foo -- ok
#check foo.1 -- failed to synthesize instance IsCommutative (NOT stuck!)
#check foo.1 h -- failed to synthesize instance IsCommutative (NOT stuck!)
def bar := foo.1 h -- failed to synthesize instance IsCommutative (NOT stuck!)
#check Iff.mp foo -- failed to synthesize instance IsCommutative (NOT stuck!)
#check Iff.mp foo h -- failed to synthesize instance IsCommutative (NOT stuck!)The last five commands should all succeed. Mathlib has a lot of lemmas like foo (usually due to CovariantClass, so e.g. le_neg, abs_pos, etc.). (It's important that the instance [CommMonoid α] → Monoid α is not a subobject projection here, but this is super common in the algebraic hierarchy.)
What's happening here is that we ignore the stuck exception in nested TC problems. So Lean thinks that the only IsCommutative instance does not apply because it cannot unify Monoid.toLeftUnit =?= CommMonoid.toLeftUnit while the type is still a metavariable. And since we ignore the stuck exception, we never try again. cc @Kha
A workaround is to specify the type manually (surprising syntax btw):
#check foo (α := Nat).1 -- ok
#check foo (α := Nat).1 h -- ok
def bar := foo (α:= Nat).1 h -- ok
For comparison, all is well without the IsCommutative argument:
theorem foo' [Monoid α] {x y : α} : x * y = z ↔ x * y = z := .rfl
#check foo' -- ok
#check foo'.1 -- ok
#check foo'.1 h -- ok
def bar' := foo'.1 h -- ok
The last five commands should all succeed. Mathlib has a lot of lemmas like
foo(usually due toCovariantClass, so e.g.le_neg,abs_pos, etc.). (It's important that the instance[CommMonoid α] → Monoid αis not a subobject projection here, but this is super common in the algebraic hierarchy.)What's happening here is that we ignore the stuck exception in nested TC problems. So Lean thinks that the only
IsCommutativeinstance does not apply because it cannot unifyMonoid.toLeftUnit =?= CommMonoid.toLeftUnitwhile the type is still a metavariable. And since we ignore the stuck exception, we never try again. cc @KhaA workaround is to specify the type manually (surprising syntax btw):
For comparison, all is well without the
IsCommutativeargument: