Library iris.algebra.monoid

Important: If you define your own monoid, only declare a Monoid instance, not a MonoidOps instance. The Monoid class is used for the generic big operators in the file algebra/big_op. The operation o and unit u are arguments instead of fields of Monoid because we want to support multiple monoids over the same carrier type (for example, on BIs we have monoids for ∗/emp, ∧/True, and ∨/False). There are two classes, MonoidOps just groups the operation and unit, while Monoid contains the laws. Definitions (e.g., the big operators) should use MonoidOps so they do not depend on proofs, while lemmas should use Monoid. In definitions, the argument o is typically given, and u is an implicit argument that is infered through search for a MonoidOps instance. Hence o has input mode, and u output mode.

Note that Monoid has an argument M : ofe. We could in principle consider monoids and big operators over setoids instead of OFEs. However, since we do not have a canonical structure for setoids, we do not go that way. Further note that we do not declare any of the projections as type class instances (i.e., we use : instead of ::). That is because we only need them in the big_op file, and nowhere else. Hence, we declare these instances locally there to avoid them being used elsewhere.

This is the only instance for MonoidOps that should exist.

The Homomorphism classes give rise to generic lemmas about big operators commuting with each other. We also consider a WeakMonoidHomomorphism which does not necessarily commute with unit; an example is the own connective: we only have True ==∗ own γ ∅, not True ↔ own γ ∅.