[ discussion ] negation via `¬_` or via `_→ Whatever`?

[jamesmckinna]

Isn't this ¬Null-∷ ? Which then doesn't need Whatever?

Originally posted by @JacquesCarette in #3091 (comment)

The discussion following this query of @JacquesCarette exposes a shift in my thinking about how best to handle

• negated propositions
• deducing consequences from them

The use of of the _→ Whatever idiom means that application alone is sufficient to do ¬-elimination, and maybe is yet another twist on 'avoid ⊥-elim where possible'...

[gallais]

Cheeky answer (had to go dig the quote up on Proof Assistants SE):

that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do.

[jamesmckinna]

Sigh. Everything that I have learnt, or taught, must be unlearnt, and learned again.

But... for me, initiality in this instance cashes out as the most usable idiom, but one which others seems to find strangely unattractive, viz. the use of an irrefutable pattern ... with () ← ... #2123

You (I) can't win!

[jamesmckinna]

(and the sound effect to accompany my reaction to @gallais 's comment above would be Anthony Hopkins as William Bligh to Mel Gibson's Fletcher Christian in "The Bounty" (1984)... "Blast you Mr. Christian, blast you!". Or maybe it was Gregory Peck to Marlon Brando in "Mutiny on The Bounty (1962)?)

In any case, ... Blast you, Sir! ... as I am set adrift in my rowing boat...

[gallais]

I also feel like ⊥-elim or contradiction has the advantage of documenting the process
by which we have reached the conclusion instead of silently invoking the pre-emptively
deployed principle of explosion.

[jamesmckinna]

Ah... the bane of expertise... the ability to make silent appeals! Compared to having to account for oneself and one's actions... "trust me, I am medically qualified"

[jamesmckinna]

#3091 fixed accordingly, and thus closing this now.

[JacquesCarette]

I've actually grown to appreciate ... with () ← ... (in proofs anyways). Irrefutable with is reasonable, conditional with is less clear. It is certainly a pain when it is used in the definition of functions.

I certainly agree with the general sentiment that explicit uses of ⊥-elim is too low level. I agree with @gallais that documenting the process of getting to the conclusion is worthwhile instead of sweeping a "first you explode then universe, then you do whatever else you want" under the carpet.

[JacquesCarette]

And maybe this discussion should have been closed after something trickled to the style guide?