Defining RAs with a partial composition operation
Right now, if your RA has a partial composition operation and you'd like to make a case distinction on something that's not decidable, you have to use some rather hideous trick. For example, in the case of STSs, composition is defined only if the intersection of the state sets is non-empty. To define this in Coq, the STS monoid actually carries around a
valid: Prop piece of "data", and equality of monoid elements is defined as a quotient, equalizing all invalid elements. @robbertkrebbers convinced me this also comes up for some other monoid, I believe it was the fractions - but actually, I can't tell any more why this should come up there. Robbert, could you remind me?
It may be a good idea to axiomatize a class of "DRAs" (disjoint RAs), that have, instead of a validity predicate, a binary disjointness predicate. Composition would still have to be total, but commutativity (and potentially associativity) would only have to hold if the involved elements are disjoint. We could then have a functor from RAs to DRAs, using above construction with the
valid: Prop and the quotient. This way, people could define such monoids much easier, but we wouldn't have to suffer the pain of using DRAs in the model. (Which would be really annoying; every time we use commutativity, we'd have to prove disjointness.)