[ refactor ] (Re)define (Is)TightApartness and (Is)HeytingCommutativeRing/(Is)HeytingField

[jamesmckinna]

Fixes #2587

Adds:

• Algebra.Apartness.Properties.HeytingField, superseding Algebra.Apartness.Properties.HeytingCommutativeRing

NB:

• latter module should now be deprecated (?) in favour of moving its one remaining property to Algebra.Properties.Ring (or even Algebra.Properties.AbelianGroup...) DONE properties moved; module NOT deprecated
• Data.Rational.Unnormalised.Properties should be refactored to make use of Relation.Binary.Properties.DecSetoid for its (Is)*ApartnessRelation definitions DONE

Issue:

• is this v2.3 (as a bug fix of the various APIs involved?) or v3.0 (as a large breaking change?)
• re: @MatthewDaggitt 's comment below about the mathematics, perhaps if someone could check what is said in eg. Troelstra and van Dalen, that might shape how this goes forward, but my own view is: authors seem to disagree about Apartness vs. TightApartness, etc. but that the fundamental distinction should be between *CommutativeRing and *Field (and yes: perhaps HeytingLocalRing would have been better, but see also Define LocalRing #2219 ) in that the latter should have inverses, while the former need not. The existing APIs make the distinction turn on whether the apartness is tight or not, which seems 'wrong'... even to the point of being a bug?

RFC from @cspollard and @bsaul ...

[MatthewDaggitt]

Otherwise, code-wise it looks good. Can't comment on the mathematics 😄

[MatthewDaggitt]

I know this is a draft, but in the final version it would be good to explain broadly what the refactorings actually are here?

[jamesmckinna]

See latest commits, hopefully enough, but not too much, detail now!

[jamesmckinna]

I think this is now ready for review! Many thanks to @MatthewDaggitt for the pre-review, hopefully the latest round of (many!) commits have put things on a more sound footing. As in updated preamble above:

• is this v2.3 or v3.0? (maybe the latter is safer? but the former is justifiable if we think the old APIs were a bug or not?)
• I've left Algebra.Apartness.Properties.HeytingCommutativeRing as an empty stub, with two deprecations, rather than deprecate the module altogether, against possible future additions to this? But in any case, as a consequence it's no longer re-exported from the new Algebra.Apartness.Properties.HeytingField module.

[JacquesCarette]

Spent a lot of time reviewing this... and no comment to speak of. I did spot several proofs that I'd want to change, but I should add some reasoning combinators first that would show how these embody repeated patterns.

[jamesmckinna]

Otherwise, code-wise it looks good. Can't comment on the mathematics 😄

Hopefully the discussion on #2587 clarifies this?

[jamesmckinna]

@JacquesCarette wrote:

Spent a lot of time reviewing this... and no comment to speak of. I did spot several proofs that I'd want to change, but I should add some reasoning combinators first that would show how these embody repeated patterns.

Much of the refactoring here (essentially code motion, little else, in service of the new, hopefully more streamlined abstractions) leaves original legacy proofs untouched. We may now have made progress elsewhere on enriching the reasoning infrastructure (have we?), so there's an opportunity here to weigh in on what you would want to change here, or else to open a fresh issue/PR documenting such. Let me know what you'd like us to do!

[JacquesCarette]

@jamesmckinna needs yet another merge. @MatthewDaggitt this is then going to be waiting on you.

[jamesmckinna]

Thanks @JacquesCarette will look at this this evening. Battling insomnia and some slightly more urgent stuff. DONE.

[jamesmckinna]

So... I did finally consult Troelstra and van Dalen (Vol.2, which is a bit harder to get hold of, and is also 2x length of Vol. 1...), and their chapter on 'Algebra' has this kind of thing largely based on a KNAW article by Heyting from 1941 which I have yet to read...

... nevertheless they draw attention to the need for additional axioms governing the relationship between _#_ and the _+_ and _*_ operators. So I'm going to push this to DRAFT for the time being, and then come back once I've added the extras back in. DONE.

Rationale: we're already making a breaking change as to the definitions of Tight and (Is)TightApartness, so we might as well get the mathematics right. Thanks to @MatthewDaggitt for drawing attention to this!

[jamesmckinna]

Candidate Algebra.Apartness.Properties.HeytingCommutativeRing (so that that module deserves not to be deprecated!):

• prove that _-_ is StronglyExtensional _#_.
• Biased smart constructors so that TightApartness and StronglyExtensional imply Congruent (and thus the underlying IsCommutativeRing axioms can be weakened.
• 0# # 1#, or else require that as part of the axiomatisation (!)

All of the above, except the last perhaps, are downstream considerations, so stopping here.

UPDATED: spoke too soon. Need to fix axiomatisation, and prove the extra pieces for Data.Rational. Ooops!

UPDATED: extra StronglyExtensional properties now proved. Moving off DRAFT for review.

[jamesmckinna]

Last call for @MatthewDaggitt to (re-)review!? I think the substance of your criticism revolved round adequately accounting for (the intent behind) this refactoring in the CHANGELOG. Plus the (hopefully correct!) re-export of (Is)ApartnessRelation and its accounting in CHANGELOG.

I'd be happy to clear this off the docket before another round of merge conflicts torpedo it...