[ add ] new name for `flip`ped version of `Relation.Nullary.Negation.Core.contradiction`

[jamesmckinna]

Workaround: You would not get this problem if contradiction had the opposite argument ordering:

contradiction : ¬ X → X → Whatever
contradiction ¬a a with () ← ¬a a

test : Whatever
test = contradiction ¬∀P ∀P

Here, the equation ¬ X = ¬ (∀ {a} → P a) is produced which solves correctly to X = ∀ {a} → P a.

Originally posted by @andreasabel in #8026

My recent woes in #2782 and my followup issue agda/agda#8026 on the main agda tracker lead me to the somewhat uncomfortable conclusion that it would be better to break the current API for contradiction by flipping its arguments, or else, perhaps more modestly, but more of a redundancy/Fairbairn threshold code smell, that we give flip contradiction a first-class name for such situations?

[JacquesCarette]

I think giving flip contradiction a first class name is a better idea. Here it is Agda itself which forces our hand. Higher concerns (redundancy, Fairbairn threshold) get derailed as 'not applicable' since contradiction and flip contradiction are not equivalent!!

[jamesmckinna]

Two followups:

• can we somehow (sensibly) reconcile the addition/modification with [ refactor ] weaken type of Relation.Nullary.Negation.Core.contradiction-irr #2785
• what name for this new lemma!? Suggestions welcome! I'd tried contradictionᵒ before... but pushback on that, including from you!

[gallais]

what name for this new lemma!?

EMP, short for Exploding Modus Ponens? 🤭

[jamesmckinna]

what name for this new lemma!?

EMP, short for Exploding Modus Ponens? 🤭

Oh! I want to be angry and humourless about this, but it has a certain something...
... that said, I'm still tempted to have a flipped contradiction-irr (with a new name, such as @JacquesCarette 's irrelevant-contradiction), and use that to drive everything? On second thoughts, coupling the two things is a terrible idea, but having three distinct combinators also seems bad!

[MatthewDaggitt]

I am against flipping the argument order for contradiction even in 3.0. It's a) it's caused by a wrinkle in Agda rather than something fundamental and b) it will break almost every piece of non-trivial code depending on the standard library in existence for a benefit in an important but still small edge case.

I am of course happy to add the flipped version as well.

[jamesmckinna]

@MatthewDaggitt I think I agree with you, essentially for the reasons you give.
(But I get the impression that the Agda wrinkle won't go away anytime soon)

We need a 'good' name for flip contradiction though, and

• previous suggestions of mine have been rejected in earlier PRs
• EMP, while hilarious, is not I think the way to go
• so... thoughts please?

[MatthewDaggitt]

Hmm I'm also struggling with meaningful names. If all else fails how about a prime symbol at the end of it? 😅