agda
Ring reasoning
Reasoning combinators for monoid, renamed and adapted for Ring. Builds on #2692 .
- I'd like to see the new semigroup properties here as well
- The semigroup properties on
*and the monoid properties on+work forRingWithoutOne - In fact, they work on
SemiringandSemiringWithoutOne, but we don't have aPropertiesmodule for those
@Taneb 's 1,2,3 above echo my thoughts on looking at these, but maybe, given our ongoing issues regarding naming in #2688 that it isn't so straightforward to back-fill the Properties for weaker structures... yet?
Guessing that this PR hints that we should perhaps also have/need the intermediate extension to Algebra.Properties.(Abelian)Group to incorporate inverse equational simplification for the +-abelianGroup sub-structure/-bundle... as a downstream PR.
Yes, there is quite a lot that can be done in this vein.
We should be careful not to have perfect be the enemy of definite-improvement...
Yes, there is quite a lot that can be done in this vein.
We should be careful not to have perfect be the enemy of definite-improvement...
Yeah, not my intention at all to obstruct this PR with demands for more here... but elsewhere, in due course, definitely!
I guess, strictly speaking, neither you nor @Taneb are blocking this on requiring more features...
Absolutely not blocking from me!
but... maybe a rebase against the new master to sort out the CHANGELOG conflict, and to catch the already-merged Semigroup commits (I think the Monoid PR I still open though...?)?
Suggest a rebase to bring this up-to-date with everything that has happened so far, esp. if you want this for v2.4
Otherwise looks fine (though I personally don't like 'short' qualified module names such as PM, rather than eg MonoidProperties), as I don't really see that saving characters is the win worth having, compared to not having to chase at least one level of indirection to figure out what is going on... but then I'm on the 'verbose' end of the spectrum ;-)