Prefer contradiction over ⊥-elim when it makes sense?

[JacquesCarette]

See PR #2652 . I think @jamesmckinna had already started down this road, this is continuing that. But I want to make sure that this is the design we want (and so should codify in style-guide).

[jamesmckinna]

As @Taneb notes on the PR, this is/can be a clear win.

My original motivation, after extensive investigation/refactoring of negation while developing Relation.Nullary.Recomputable and its consequences, was to try to avoid explicit appeal to ⊥-elim altogether, in favour of contradiction etc. as an encapsulated abstraction.

This would/could subsequently be weakened to permit further exploitation of the irrelevance of arguments of negated type. See #2346

So I'm definitely in favour!

[JacquesCarette]

So I'm going to let @jmougeot know that he can go ahead and submit PRs to continue this - but single-file PRs for this, as I suspect some of them will not be 'clear wins'.

[jamesmckinna]

One other thing I have suggested in the past is also to replace explicit use of = ⊥-elim p with with () ← p... in the 'other' cases.

I still regard that, in and of itself, as a 'clear win', but the lack of response to #2123 suggests/suggested that I was, perhaps, alone in thinking that... and in my jeremiad against overly explicit exposure of the underlying representation of ⊥ (part of a wider issue about how much we are willing to sacrifice 'abstractness' in the library API in favour of exposing such representations...)

[jamesmckinna]

So I'm going to let @jmougeot know that he can go ahead and submit PRs to continue this - but single-file PRs for this, as I suspect some of them will not be 'clear wins'.

Indeed, regarding adding this to the style-guide, it might be worth canvassing beyond my own (perhaps) idiosyncratic opinion...

[gallais]

I thought it was already in the style guide as @MatthewDaggitt has been pushing
for contradiction over ⊥-elim pretty consistently in the past.

[jamesmckinna]

I thought it was already in the style guide as @MatthewDaggitt has been pushing for contradiction over ⊥-elim pretty consistently in the past.

Sadly, not in style-guide (yet)... but good to know that you and @MatthewDaggitt agree!

[jamesmckinna]

Hmmm... the granularity of the stream of incoming PRs (eg. #2655 and #2657 ) is on a per-use basis, rather than a per-module basis. Does this make sense? It ends up that neither PR is able to remove the import of ⊥-elim!
Suggest squashing these things together to a more meaningful unit of change? Shout-out to reviewer @Taneb for comment...

[jmougeot]

There are about twenty files left to group. Should I merge them into a single PR or split them into smaller ones?

[jamesmckinna]

I'd be happiest with '1 module = 1 PR' level of granularity (I think) and I had been presuming that that was @JacquesCarette 's original intention?

[jmougeot]

Yes, I'm already doing that, the names of PRs are confusing since I wrote the name of the module I changed. It just means that there's no other change to do in this file.

[jamesmckinna]

Yes, I'm already doing that, the names of PRs are confusing since I wrote the name of the module I changed. It just means that there's no other change to do in this file.

Well, the two examples I cited concern the same module: Relation.Binary.Consequences?
And as for the names of PRs, yes they are confusing, but that's something you can change!

[jamesmckinna]

For the sake of discussion, and definitely not to derail the PR train, but thinking about the prevalence of eg contradiction refl as a pattern (in a context of a Reflexive relation, and a hypothetical instance of being Irreflexive) , but I wonder about a larger-scale refactoring around minimal logic versions of 'negation' wrt an arbitrary false/Whatever, and then instantiating those properties at a certain point with false = ⊥... and while I see that some of the machinery exploits such representation, whether or not it could benefit from being more systematic...?