Zulip Chat Archive
Stream: new members
Topic: overlapping monoid instances (bad diamond?)
Hannah Fechtner (Oct 07 2024 at 22:09):
A simplified version of my problem : I want to prove theorems about presented monoids which are cancellative.
I have defined a presented monoid over some relations (by quotienting a free monoid by the relations). I have proved that this PresentedMonoid rels
is an instance of a Monoid
.
But my theorem about cancellative presented monoids cannot take in, say, [CancelMonoid (PresentedMonoid rels)]
, for then Lean won’t know why PresentedMonoid rels
is a monoid — PresentedMonoid is a monoid, and a CancelMonoid is a monoid.
For the moment, I have been using hypotheses like (cancel_left : \forall a b c, a * b = a * c \to b = c)
The full problem requires 5 such hypotheses, which feels unwieldy. I can bundle them into a tuple, but it really feels like it should be an instance/class kind of construction.
My other idea was to define a class PresentedMonoid
, with data of the underlying set, the relations, and then a theorem stating the universal property. Then I could use the extends
keyword to add in, say, CancelMonoid
to get CancelPresentedMonoid
. (I am skeptical because PresentedGroup is not a class, so probably my PresentedMonoid shouldn’t be either).
Is either of the two ways preferable? Is there another way? Thank you!
Kevin Buzzard (Oct 08 2024 at 07:18):
I'm not sure I've understood your problem correctly -- is the issue that you have a monoid and want to beef it up to a CancelMonoid in the middle of a proof? If so then you can do somthing like this:
import Mathlib.Tactic
example (M : Type*) [Monoid M] (h : ∀ (a b c : M), a * b = a * c → b = c) : True := by
letI : LeftCancelMonoid M := {
toMonoid := inferInstance
mul_left_cancel := h
}
sorry
Apologies if I've misunderstood.
Hannah Fechtner (Oct 08 2024 at 15:22):
thanks! that was one hurdle I've gotten through
perhaps this will explain it better:
Say I've proved that for some specific set of relations (call them rels1
), that PresentedMonoid rels1
is in fact cancellative; that I have
instance [CancelMonoid (PresentedMonoid rels1)]
, via something like
instance : CancelMonoid (PresentedMonoid rels1) where
mul_left_cancel := cancel_left_rels1
mul_right_cancel := cancel_right_rels1
That's all well and good. Now when I go to state a theorem about cancellative presented monoids, what should I do in my assumptions? I cannot use [CancelMonoid (PresentedMonoid rels1)]
as I get some kind of "bad diamond" because there are two ways to infer the monoid instance. At the moment, I have been passing in cancel_left_rels1
and cancel_right_rels1
as arguments every time. It just seems like there should be a better way to write theorems about cancellative presented monoids
I guess my question is, what's the best way to set up the assumptions for a theorem?
Eric Wieser (Oct 08 2024 at 16:02):
You can use [IsCancelMul (PresentedMonoid rels1)]
Last updated: May 02 2025 at 03:31 UTC