[ breaking ] Flip arguments to `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?