[ 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 #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]

Latest commit rejigs the statements in terms of instance arguments for Except_-*Cancellative_, but it's not obvious to me that the ergonomics actually improve? (This may be to do with lemma statements whose explicit quantifier structure interferes with instance inference?) I guess more experimentation with the other numeric types is required...

[jamesmckinna]

I think I can't face doing more with this PR at this stage: the new definitions are in-place, with one specimen instantiation for Nat, but it isn't clear to me how best to proceed with:

• [ ] the rest of Data.Nat.Properties
• [ ] Data.Integer.Properties
• [ ] Data.Rational.Properties

without a lot more refactoring, which I suggest take place downstream?

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

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