Decidable Setoid -> Apartness Relation and Rational Heyting Field

[cspollard]

As requested on zulip, this adds

1. a proof that all Decidable Setoids induce a tight Apartness Relation and
2. a proof that the Rationals form a Heyting Field.

I hope I've properly followed relevant conventions. I wasn't sure if it was appropriate to add new files here: I can re-organize if needed. Some of the lemmas may exist elsewhere and/or could be exported.

[jamesmckinna]

Chris, that looks great, thanks!

Apologies for not having followed the discussion on Zulip, where some of the issues below could have been handled ahead of this PR...

UPDATED: Apologies also to @guilhermehas for not having paid attention to #1959 before charging ahead with my review...

Detailed review to follow, but headine comments as follows:

Under item 1

• the negated equality symbol is already defined as part of Relation.Binary.Bundles.Setoid, so no need to redefine it;
• the proof that it is symmetric is already in Relation.Binary.Properties.Setoid, so should be imported from there;
• that's moreover the better place to put the proof of Irreflexive;
• leaving only Relation.Binary.Properties.DecSetoid to have the proof of Cotransitive, and hence the structure isApartnessRelation : IsApartnessRelation ... and bundle apartnessRelation : ApartnessRelation (again: the names are by convention, also, being that the record instance is named for the lower-case-first-but-otherwise-camelcase of the corresponding record type, as in your Heyting module); the other properties can be reimported from Setoid...; the ambient general principle being that things should live in the hierarchy at the place of maximum generality, and be (re-)exported if need be from more specialised instances

Under item 2, similarly:

• the Group properties of subtraction should follow automatically from Algebra.Properties.(Abelian)Group, based on the corresponding structure(s)/bundle(s) defined in Data.Rational.Properties;
• the subsequent properties don't really need to be in a separate module, but can simply be added to the above Data.Rational.Properties, on the model of all the other structures and bundles defined there...

And, of course, a CHANGELOG entry will be needed. Given that this will probably not get merged before v2.1, it might be easier to hold off on this last step until the v2.0 release, with consequent re-set of the CHANGELOG to a blank... but @MatthewDaggitt can advise on that!

[cspollard]

Thanks @jamesmckinna this is really helpful. I hope to come back soon with the updates. I don't feel strongly about which release this targets -- whenever you and @MatthewDaggitt feel is appropriate.

[jamesmckinna]

Revised review incoming. Highlights:

• names of variables etc. in Data.Rational.Properties should be p, q, r etc. rather than i, j (used for Integers); see doc/style-guide.md for these things;
• imports; the Algebra.Bundles and Relation.Binary.Bundles have been carefully designed to both be layered in terms of how the richer structures are built up from simpler ones, while at the same time public re-exporting the nested substructures, so for DecSetoid, quite a lot (in fact: all, in this instance I think) of those imports can be flattened;
• use of where clauses to make local/private lemmas on the way to the main results regarding *Heyting*; it's tempting to try to make things as tight as possible, but given the ability to exploit using clauses/qualified module imports, then it's usually preferable to leave all the 'smaller' lemmas as publicly visible at the module top-level. If there's any question of name clash, one can revisit such decisions, but otherwise, if something is useful, it might be useful elsewhere. But I can see that's sometimes a tricky judgment call.

Otherwise minor things:

• within the scope of Data.Rational.Properties, it's OK to exploit the fact that equality is propositional, and in particular to make use of refl where possible...;
• implicit vs. explicit quantification: what you have tends towards explicit quantification, but some of that could be tightened up. Again a judgment call, but my inclination is towards more implicits where possible without loss of intelligibility...

[jamesmckinna]

@cspollard I realise (belatedly!) that I may have come across as too tyrannical (for a relative newcomer) in my demands for refactoring in favour of stdlib style guidelines. I'd be happy to push commits which follow those guidelines/my review comments, if that makes your life easier. But it would be good if you also pushed a CHANGELOG commit, ... eventually.

[cspollard]

Hi @jamesmckinna don't worry! Getting a coherent style in the lib is important, and I don't mind updating this. I am just stuck in a combination of teaching and traveling at the moment. I should be able to come back to this in the next 10 days or so -- sorry for the delay.

[jamesmckinna]

No worries about the delay... it won't get merged until after the v2.0 release, which is experiencing the predictable hiccups as we iron out last things...

... in the meantime: safe travels!

[jamesmckinna]

Hmmm, maybe it's good that there is a pause in proceedings after all. If you look carefully in Data.Rational.Unnormalised.Properties, then (almost) all of the proofs here, and definitely the Structures and Bundles for this PR are already present... soooo:

• please (re-)consider the proofs/constructions for Data.Rational.Properties by lifting those from the Unnormalised ones, rather than re-proving from scratch;
• please also see if the constructions in the Unnormalised case can be simplified using the Algebra/Relation.Binary properties you have developed here (that's perhaps a separate, subsidiary, refactoring PR?)

I'm really sorry not to have paid attention to this before in my review! It would be shame to continue with what might simply be duplicate work, if instead that can be (considerably?) simplified/refactored. Suggest perhaps converting this PR to DRAFT in the meantime?

[cspollard]

Hi @jamesmckinna @MatthewDaggitt Thanks for the feedback!

Good to know about the Unnormalized properties from @guilhermehas ! I will have a go at re-using these where possible.

I would suggest that I push a reformulated version in a few days, trying to incorporate the editorial comments at the same time. I will probably need at least one more pass of feedback after that, since it will be a fairly invasive set of changes.

Happy holidays.

Chris

[jamesmckinna]

Happy New Year @cspollard ! Any progress on this, or do you want some help?

[cspollard]

Hi. I'm sorry for the delay, but during term I really struggle to make time for new developments, regardless of my best intentions. I'm hoping to put some time in this and next week, now that teaching is done for a bit.

I stumbled upon Algebra.Construct.Subst.Equality recently. Is there a similar set of constructs for Carriers that are isomorphic? i.e., if A and B are isomorphic, and A has some algebraic structure, then B will share this same structure via the isomorphism. If we had something along these lines for the Apartness-related algebraic structures, then I could use the instance that already exists for unnormalized rationals by using the isomorphism between unnormalized and normalized rationals.

If that sounds over-complicated, I can just try to plow forward directly with the normalized rationals.

[jamesmckinna]

Chris, commiserations about the burdens of teaching, good to know you can see light at the end of the tunnel.

Regarding the PR and your latest comment:

• going via Isomorphism of structures would/might be great, but we don't have a lot of/any infrastructure for that cf. #2102 #2113 ;
• an important principle (and physician: heal thyself!) for PRs, in the interests of closure..., is to not let the perfect be the enemy of the good, even at the cost of needing to subsequently refactor... so I would go for the 'low road' of what you already have done; otherwise we get into the inertia/death-spiral of PRs withering on the vine thanks to subsequent developments (eg see the recent merge conflicts: let us know if you want/need help with this)

So: suggest you plow on, but I think there shouldn't be much else to do?

[jamesmckinna]

I resolved the merge conflict (plus a fix-whitespace), but UPDATED: I no longer think that each of your additional lemmas in Algebra.Properties.group are/should be now easy consequences of lemmas in Loop or Quasigroup.~~so further refactoring may be possible.~~ Rather they are/seem to (specialised! versions of) the 'converse' properties to Algebra.Properties.Quasigroup.y≈x\\z and x≈z//y, and that does require the Group structure...

... so you could consider renaming them to fit that schema?

UPDATED: I have left them named as they were for the time being, and tidied up the below-Fairbairn-threshhold contrapositives...

[jamesmckinna]

Apologies for taking control of this from you @cspollard , but I've taken the liberty of resolving all of the above conversations by pushing a bunch of commits, in the interests of closing this sooner rather than later, but have managed once again to ignore my own comments above about the Unnormalized case.

That said, and again in the interests of closing this off as soon as possible, suggest such refactoring be considered as a downstream PR...?

And, in the meantime, request a second review from @MatthewDaggitt please, and from an independent third-party... @Taneb ?