[ 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.

[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?

[JacquesCarette]

I'm still not quite getting it. o m n is a bizarre order, m n o is better. But that's just order of the variables. You probably mean something deeper that is clear in your head, but probably need to unwind some layers of definitions to see?

Re: *-cancelʳ-≤-neg. The fact that ≤ becomes ≥ in the conclusion is highly non-trivial. It's just seems trivial to use because of how long ago we've integrated the action of negatives on ordering relations into our knowledge base. The point is that this isn't 'structural' in any reasonable way, so there is no actual pattern to be leveraged here (well, there is, but it's too general to be of much use in practice, IMHO).

[jamesmckinna]

Merge conflict fixed (including fixing some typos in CHANGELOG!), and so what's left

• as I understand @JacquesCarette comments above, we shouldn't try to (over-)generalise to multiple relations as part of this PR
• not yet fixed the argument order, but I'm tempted simply to not try this time around!

If you think this is mergeable, I'll let go for the time being.

[JacquesCarette]

I think this PR is a good unit of progress as-is.

[jamesmckinna]

Not quite sure how to go back to this after more than a year... and all the merge conflicts are definitely a headache!

[jamesmckinna]

Merge conflicts are one thing, but I think I'd (now!? v3.0 etc.) like to be more radical in making this breaking, by simply changing the API to make Almost* offer the positive/constructive/disjunctive version only. Comments welcome!

[jamesmckinna]

Beyond considerations of what this PR might/should actually contain, I've brought it up to date, and with two approvals from @JacquesCarette and @MatthewDaggitt suggest merging now/soon and then seeing how the dust settles?

[JacquesCarette]

I agree with my past self: this PR, as of today, is a worthwhile series of improvements.

The more radical version might be good too, but feels like a new step, best performed on top of this one.