Algebra property reexports

[Taneb]

• Note that a RingWithoutOne is a SemiringWithoutOne
• Introduce new module Algebra.Properties.SemiringWithoutOne
• Re-export many algebraic properties (appropriately renamed) into the property files for larger algebraic structures, including all the new semigroup properties for semirings, both for addition and multiplication

[Taneb]

Ah - this is failing, in part because I assumed that what I was calling +-cancelʳ (specialization of Properties.Semigroup.cancelʳ to addition) matches the preexisting +-cancelʳ (addition is right cancellative). There needs to be some rethinking of names here.

[jamesmckinna]

Ah - this is failing, in part because I assumed that what I was calling +-cancelʳ (specialization of Properties.Semigroup.cancelʳ to addition) matches the preexisting +-cancelʳ (addition is right cancellative). There needs to be some rethinking of names here.

See also #2654 ... I think there this is (yet another) instance of systematic clash of different authors' mental models of what the qualifiers denote... ?

Er, no. It's because we accepted the Algebra.Properties.Monoid.cancel* in #2692 without thinking through the consequences wrt Cancellative operations. Sigh.

[jamesmckinna]

I've made (frankly unsatisfactory) suggestions as to how to rename things, otherwise I'd simply approve. This all looks like useful refactoring/filling in the hierarchy, but we do need to do something about these cancel lemmas...

[jamesmckinna]

Actually, I think it might be easier to simply not export the 'offending' names, on the basis that

• this should guarantee that testing succeeds (?)
• that this doesn't commit to 'nonsense' names ahead of any refactoring/renaming in Algebra.Properties.Monoid

Thoughts?

[JacquesCarette]

In theory, this is good. In practice, clearly there are all sorts of problems. Which require non-trivial thinking, which I can't do right now. But will come back to this when I can.

[jamesmckinna]

In theory, this is good. In practice, clearly there are all sorts of problems. Which require non-trivial thinking, which I can't do right now. But will come back to this when I can.

Hope you manage to find space/time/brainspace to do this... you have far-reaching insights into how to improve Algebra.* general, and stdlib needs them! #2765 etc.

My current thinking about the cancel* properties is that they be renamed to inverse⇒cancel* (I know you don't like long names, but such 'implicational' forms do, at least, reflect the logical structure), and they certainly could be, locally here, in order to not obstruct progress? See #2885 for specimen usage.