Library iris.algebra.monoid

The Monoid class that is used for generic big operators in the file algebra/big_op. The operation is an argument because we want to have multiple monoids over the same type (for example, on uPreds we have monoids for ∗, ∧, and ∨). However, we do bundle the unit because:

• If we would not, it would appear explicitly in an argument of the big operators, which confuses rewrite. Now it is hidden in the class, and hence rewrite won't even see it.
• The unit is unique.

We could in principle have big ops over setoids instead of OFEs. However, since we do not have a canonical structure for setoids, we do not go that way. Note that we do not declare any of the projections as type class instances. 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.

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 γ ∅`.