[ refactor ] Revise definitions, consequences, and use, of Algebra.Definitions.(Almost)*Cancellative

[jamesmckinna]

Fixes #1436 , ...
... at least as far as 'AlmostCancellative' properties of operations wrt equality relation; the various order-theoretic generalisations are not covered
... so the issue probably ought to be kept open even if this gets merged? cf. #2580

NB.:

• see issue for discussion of the design strategy (could be less breaking? naming issues... etc.)
• Algebra.Consequences.Base refactoring [ refactor ] Add equality as a parameter to Algebra.Consequences.Base #2572 should probably be merged first; fold in the instance-based analysis for Decidable (and hence Recomputable) predicates into Except_-*Cancellative_?
• only equality-based properties tackled so far... Algebra.Definitions only imported at the equality relation, but might better be left parameterised, so that the various Cancellative properties can be made generic...
• for Integer and Rational, the Cancellative properties wrt multiplication don't easily cash out via the 'generic' design strategy of going via AlmostCancellative, so I haven't (yet) include such statements, nor refactored to make these the primary notions.

[JacquesCarette]

Seems like a nice PR as-is, more can be done subsequently.

[jamesmckinna]

Seems like a nice PR as-is, more can be done subsequently.

Thanks @JacquesCarette I suppose my concern was that if it turned out those downstream PRs were still stymied by 'bad' design decisions here, then ... I'm not sure what. Certainly it seemed a big job to try to refactor existing proofs to try to conform to the new APIs...

[JacquesCarette]

To allay your fears, might be worth taking Data.Rational.Properties (in a new branch based off of this one) and porting it, but without aiming to make that port a PR, just a "is this a good idea" test.

[jamesmckinna]

To allay your fears, might be worth taking Data.Rational.Properties (in a new branch based off of this one) and porting it, but without aiming to make that port a PR, just a "is this a good idea" test.

So to allay the fears about whether it's too much work to make the change, I may as well (accept having to) do the additional work to make the change? Sigh...

[JacquesCarette]

So to allay the fears about whether it's too much work to make the change, I may as well (accept having to) do the additional work to make the change? Sigh...

Well, it might turn out to be easy! Or you might be right, and be able to estimate just how much work it is, and let us know.

[MatthewDaggitt]

There are lots of good changes in here, but it's difficult to parse all the different definitions of cancellative being added. I'll have another look if you can lay them out on separate lines?

[jamesmckinna]

Ditto.

[jamesmckinna]

Besides the still-outstanding merge conflict, some improvement (I hope!) in the CHANGELOG documentation of the API change(s).

[jamesmckinna]

Drawback 1.

OK... I might need to go back to the drawing board, a bit, now that we have, for Data.Nat.Properties (L927-L931):

*-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
*-cancelʳ-≡ m n o = almost⇒exceptʳ _ *-almostCancelʳ-≡ o m n {{≢-nonZero⁻¹ _}}

*-cancelˡ-≡ : ∀ m n o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n
*-cancelˡ-≡ m n o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n o

as the status quo ante, and with the new definitions, instead we would have (NB: argument order!)

*-cancelʳ-≡ : Provided NonZero RightCancellative _*_
*-cancelʳ-≡ m n o = almost⇒exceptʳ _ *-almostCancelʳ-≡ m n o {{≢-nonZero⁻¹ _}}

*-cancelˡ-≡ : Provided NonZero LeftCancellative _*_
*-cancelˡ-≡ m n o rewrite *-comm m o | *-comm m n = *-cancelʳ-≡ m n o

So...: what is/should be the correct argument order in all the new definitions, or do we simply carry on breaking the API?

[jamesmckinna]

Drawback 2.

Suppose we want to rewrite eg. Data.Nat.Properties L967-973

*-cancelʳ-≤ : ∀ m n o .{{_ : NonZero o}} → m * o ≤ n * o → m ≤ n
*-cancelʳ-≤ zero    _       _         _  = z≤n
*-cancelʳ-≤ (suc m) (suc n) o@(suc _) le =
  s≤s (*-cancelʳ-≤ m n o (+-cancelˡ-≤ _ _ _ le))

*-cancelˡ-≤ : ∀ o .{{_ : NonZero o}} → o * m ≤ o * n → m ≤ n
*-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o

to use the new definitions, then, modulo Drawback 1., we would (be able to) have:

*-cancelʳ-≡ : Provided NonZero RightCancellative _*_
*-cancelˡ-≡ : Provided NonZero LeftCancellative _*_

modulo fiddling the imports so that we replace _≡_ with _≤_ in the definitions... so far so good.

BUT: for Data.Rational.Properties L1360, we can't rewrite:

*-cancelʳ-≤-neg : ∀ r .{{_ : Negative r}} → p * r ≤ q * r → p ≥ q

in terms of Provided Negative RightCancellative _*_... because the relation in the conclusion has flipped. So... probably, everything should move to Relation.Binary.Definitions to allow independent parametrisation on the two relations, and then import those definitions in Algebra.Definitions instantiated at the same relation.

My brain hurts. Doable, but exhausting... :-( And see all the other drawbacks (unsolved metas) which arise in #2580 ...

[jamesmckinna]

(Potential) Drawback 3.
Are all/any of the other potential uses of the Provided/Except family of properties expressible as 'algebraic' instances of Almost, for suitable choices of the underlying 'equality' relation in terms of some e?

UPDATED: yes, sort of, but will require the generalisations to multiple relations considered under 2. above.

[JacquesCarette]

From the code you show, the argument order seems fine? Is there something I'm missing?

It also seems to me that it is *-cancelʳ-≤-neg that is weird, not what you've written. It inlines a 'relative complement' operation in its type, which isn't something generic combinators really should be expected to deal with, not unless we over-generalize.

[jamesmckinna]

Re: argument order
It's more a question: do we try to keep the old order of arguments (o m n in the above example), or commit to the new order induced (m n o) by the particular 'design' of the new predicates. Otherwise put: should the new predicates be redesigned to retain the old argument order (fiddly, but doable, I think, and maybe not even sensible, but I've lost the capacity to resolve such decisions)

Re: *-cancelʳ-≤-neg
I think I don't quite understand your comment? It's 'obviously' a cancellation property, but the 'flip'/generalisation in the conclusion ordering arises because of the nature of the proviso Negative r... so I don't quite see how the 'relative complement' plays a role?