math-comp
Generalize lemmas from monoid to semigroups
Motivation for this change
Many lemmas for bigops on monoids (particularly abelian ones) were already valid on (abelian) semigroups. This generalization could be improved by adding semigroups to the monoid hierarchy, when porting to HB.
Some lemmas don't require a monoid with a neutral element but only an idempotent element. This is particularly useful for min/max that are idempotent but generally don't have a neutral element.
This is used for min/max in Analysis: https://github.com/math-comp/analysis/pull/712
Things done/to do
- [x] added corresponding entries in
CHANGELOG_UNRELEASED.md(do not edit former entries) - [ ] ~added corresponding documentation in the headers~
Automatic note to reviewers
Read this Checklist and make sure there is a milestone.
@affeldt-aist this seems reasonably ready for nearly three months now, would you assign and merge?
@affeldt-aist this seems reasonably ready for nearly three months now, would you assign and merge?
I would have said okay a few days ago but the generalization requested in https://github.com/math-comp/analysis/pull/779 seems (at first sight) to trigger generalizations here also. I will try to investigate this by the end of the week.
@affeldt-aist I had a look at https://github.com/math-comp/analysis/pull/779 , this made me add big_undup_AC here.
There are certainly other things from the mathcomp_extra.v file from analysis to backport to matchomp, but I think this backporting belongs to a further PR.