overlapping monoid instances (bad diamond?)

Stream: new members

[Hannah Fechtner]

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]

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]

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]

You can use [IsCancelMul (PresentedMonoid rels1)]