[ 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've now added more detail here since your most recent round of review, asking, as I understood it, for the CHANGELOG to better account for what's going on here.

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

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

[MatthewDaggitt]

Other than that, looks good.

[MatthewDaggitt]

We seemed to have removed a lot of definitions from this file without either re-exporting them from elsewhere, deprecating them or documenting it in the CHANGELOG? Maybe I'm missing something though...

[jamesmckinna]

OK, thanks for this.

I think I had (at least!) two/three/four problems:

• needing to move code from HeytingCommutativeRing to HeytingField (specifically, the invertibility properties you highlight) but without renaming/deprecation, because not wanting to invent 'bogus' new names for the sake of standardising things apart (or: dependency cycles!? they can't be re-exported from HField to HCRing...); this is a 'bug' in the original definitions, so, or so I thought, needing 'fixing' by putting things in the 'right' place...
• changing certain other definitions (specifically Tight as a property of an ApartnessRelation) to better account for the original intention behind the (Is)Heyting* definitions
• adding the 'official' Heyting-like properties of the algebra operations being suitably 'congruential' wrt apartness, by positive phrasing the analogues of the contrapositives of Congruent (cf. Cancellable etc.)
• how best to account for these things in the CHANGELOG.

I clearly need to do better as to the last point, so I'll have another go at fleshing out what's what here...