Sharing bigop lemmas between monoids and idempotent semigroups (bands)

[pi8027]

I wanted to implement this idea in bigop.v but never had time for that. So, I'm briefly writing my idea here.

Many lemmas about \big[op/idx] require idx to be the identity element w.r.t. op. However, we know that we sometimes do not have the identity element, e.g., when op is meet or join of a lattice without top and bottom.

It seems to me that many lemmas about \big[op/idx] can be generalized to require only:

• op is associative (and sometimes commutative), and
• idx is idempotent w.r.t. op, i.e., op idx idx = idx.

For a monoid (T, ⋅, e), e is idempotent w.r.t. ⋅. For an idempotent semigroup (also called band) (T, ⋅), any element x : T is idempotent w.r.t. ⋅. Therefore, the above structure enables sharing of lemmas between monoids and idempotent semigroups.

I'm not sure whether we can implement the latter inheritance (from idempotent semigroups) using canonical structures because the idempotent element is arbitrary.

[proux01]

It seems to me that many lemmas about \big[op/idx] can be generalized to require only:

* `op` is associative (and sometimes commutative), and

* `idx` is idempotent w.r.t. `op`, i.e., `op idx idx = idx`.

Note that we already have quite a few of those lemmas (look for _idem in bigop.v) but maybe more can be generalized.

For a monoid (T, ⋅, e), e is idempotent w.r.t. ⋅. For an idempotent semigroup (also called band) (T, ⋅), any element x : T is idempotent w.r.t. ⋅. Therefore, the above structure enables sharing of lemmas between monoids and idempotent semigroups.

We don't have idempotent semigroups currently but maybe that would be a structure worth adding indeed, at least considering that min and max are common instances.

I'm not sure whether we can implement the latter inheritance (from idempotent semigroups) using canonical structures because the idempotent element is arbitrary.

It's also a bit unclear to me how that would fare but that could be something interesting to try (I mean adding structures SemiGroupWithIdElem idx and IdempotentSemiGroup).

[pi8027]

To support the case where there are several idempotent elements, the idempotence structure should take op as a parameter rather than bundling it.

[proux01]

Not sure I get the point, I get why idx should be a parameter (just like it currently is for monoids) but what do we gain by also making op a parameter? Do we have an interesting use case were we have two very different idempotent elements?

[pi8027]

If the structure I proposed above (semigroup + an idempotent element idx) takes idx as a type parameter, its instance declaration fixes idx. Then, we actually cannot represent a band, where any element is idempotent, as its extension.

[proux01]

Yes and no, the instance can range over a family of idx, maybe this can be enough.