Adding new reasoning combinators

[JacquesCarette]

Fascinating how these next proofs are essentially the cancel and elim (left and right) combinators in Categories.Morphism.Reasoning !

Originally posted by @JacquesCarette in #2251 (comment)

The point would be that for binary operations for which we have congruence (i.e. everything above Magma), there are additional combinators that we can create. Even more above Semigroup, where we also get associativity, and also Monoid (unital).

So we should get more and more reasoning power as we move up.

EDIT:
Categories.Morphism.Reasoning

[jamesmckinna]

Naming:

• Is cancel actually an instance of a Cancellative property?
• Is there a more memorable/less generic name than elim for the other one?

[JacquesCarette]

• No, as Cancellative have a different shape and cancel-left: x * y = e -> x * (y * z) = z for e a unit. It is a chain of assoc, apply on left, left-unit. (There's cancel-right too).
• elim-id would be slightly better. The comments above the definition of those combinators is

-- Introduce/Elimilate an equivalent-to-identity
-- on left, right or 'in the middle' of something existing

[jamesmckinna]

Looks worth pursuing! ... perhaps provided there are concrete instances in the library that could usefully be refactored to exploit these new combinators? (Hint: any PR introducing them should at least attempt to do an amount of such refactoring as well?)

[jamesmckinna]

Further thoughts: already in Algebra.Consequences.* and Algebra.Properties.* there are examples of this kind of 'layered' reasoning, but what the combinators defined there don't seem to do is to build in associativity etc. in order to build larger hypothetical proof steps, relying instead on vanilla appeals to cong, trans etc. via Relation.Binary.Reasoning.Setoid... so as elsewhere, suggest revisiting Larry Paulson's original LCF work on 'conversions' and 'conversionals', as well as the general principle that sometimes, in any category/reflexive-transitive composition structure, there's a balance to strike between constructing arrows/proofs out of whole cloth, by composition, and letting Yoneda do some (more) of the work for you.

[jamesmckinna]

Will the various recent PRs which attempt to add various Algebra.Properties.* in a layered fashion (#2851 #2692 ...) end up closing this issue, or does it remain open for ever and a day as a reminder to appropriately 'layer' such principles/combinators.

[JacquesCarette]

No issue should ever remain open forever. We should limit the scope of this one and open new ones when we want to expand the scope.