[ refactor ] make contradiction and friends entirely definitionally proof-irrelevant

doc/style-guide.md

@@ -721,4 +721,5 @@ systematic for `Nary` relations in PR
 
 Where possible use `contradiction` between two explicit arguments rather
 than appealing to the lower-level `Data.Empty.⊥-elim`. This provides
-clearer documentation for readers of the code.
+clearer documentation for readers of the code, but also permits a wider
+range of application, thanks to its arguments being made proof-irrelevant.

src/Algebra/Module/Properties/Semimodule.agda

@@ -16,10 +16,13 @@ module Algebra.Module.Properties.Semimodule
   (semimod   : Semimodule semiring m ℓm)
   where
 
+open import Relation.Nullary.Negation using (contraposition)
+
 open CommutativeSemiring semiring
 open Semimodule          semimod
 open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid
-open import Relation.Nullary.Negation using (contraposition)
+
+------------------------------------------------------------------------
 
 x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ
 x≈0⇒x*y≈0 {x} {y} x≈0 = begin

src/Data/Fin/Properties.agda

@@ -1071,7 +1071,8 @@ search-least⟨¬_⟩ {P = P} P? =
 
 ¬∀⇒∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
                  ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
-¬∀⇒∃¬-smallest n P P? ¬∀P = [ contradiction′ ¬∀P , lemma ] $ search-least⟨¬ P? ⟩
+¬∀⇒∃¬-smallest n P P? ¬∀P =
+  [ (λ ∀P → contradiction′ ¬∀P ∀P) , lemma ] $ search-least⟨¬ P? ⟩
   where
   lemma : Least⟨ ∁ P ⟩ → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
   lemma (least i ¬pᵢ ∀[j<i]¬¬P) = i , ¬pᵢ , λ j →
@@ -1080,7 +1081,7 @@ search-least⟨¬_⟩ {P = P} P? =
 ¬∀⇒∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
           ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
 ¬∀⇒∃¬ n P P? ¬∀P =
-  [ contradiction′ ¬∀P , (λ (least i ¬pᵢ _) → i , ¬pᵢ) ] $ search-least⟨¬ P? ⟩
+  [ (λ ∀P → contradiction′ ¬∀P ∀P) , (λ (least i ¬pᵢ _) → i , ¬pᵢ) ] $ search-least⟨¬ P? ⟩
 
 -- lifting Dec over Unary subset relation
 
@@ -1103,7 +1104,7 @@ decFinSubset {suc _} {P = P} {Q = Q} Q? P? = dec[Q⊆P]
 
   dec[Q⊆P] : Dec (Q ⊆ P)
   dec[Q⊆P] with Q? zero
-  ... | no ¬q₀ = map′ (cons (contradiction′ ¬q₀)) Q⊆P⇒Q⊆ₛP ih
+  ... | no ¬q₀ = map′ (cons (λ q₀ → contradiction′ ¬q₀ q₀)) Q⊆P⇒Q⊆ₛP ih
   ... | yes q₀ = map′ (uncurry (cons ∘ const)) < _$ q₀ , Q⊆P⇒Q⊆ₛP > (P? q₀ ×? ih)
 
 ------------------------------------------------------------------------
@@ -1155,7 +1156,7 @@ injective⇒existsPivot {f = f} f-injective i
   fj<i : (j : Fin′ (suc i)) → f (inject! j) < i
   fj<i j with f (inject! j) <? i
   ... | yes fj<i = fj<i
-  ... | no  fj≮i = contradiction (_  , ℕ.s≤s⁻¹ (inject!-< j) , ℕ.≮⇒≥ fj≮i) ¬result
+  ... | no  fj≮i = contradiction′ ¬result (_  , ℕ.s≤s⁻¹ (inject!-< j) , ℕ.≮⇒≥ fj≮i)
 
   f∘inject! : Fin′ (suc i) → Fin′ i
   f∘inject! j = lower (f (inject! j)) (fj<i j)

src/Data/Nat/Primality.agda

@@ -22,7 +22,8 @@ open import Function.Base using (flip; _∘_; _∘′_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Nullary.Decidable as Dec
   using (yes; no; from-yes; from-no; ¬?; _×?_; _⊎?_; _→?_; decidable-stable)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂)
+open import Relation.Nullary.Negation.Core
+  using (¬_; contradiction; contradiction′; contradiction₂)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core
@@ -347,8 +348,9 @@ irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2
 ... | s<s z<s = inj₂ refl
 
 irreducible⇒nonZero : Irreducible n → NonZero n
-irreducible⇒nonZero {zero}    = flip contradiction ¬irreducible[0]
-irreducible⇒nonZero {suc _} _ = _
+irreducible⇒nonZero {zero}  irreducible[0] =
+  contradiction′ ¬irreducible[0] irreducible[0]
+irreducible⇒nonZero {suc _} _      = _
 
 irreducible? : Decidable Irreducible
 irreducible? zero      = no ¬irreducible[0]

src/Relation/Nullary/Negation.agda

@@ -72,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (contradiction′ ¬a) ¬a
+call/cc hyp ¬a = hyp (λ a → contradiction′ ¬a a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -82,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Product.map₂ const (f p)
-  helper (no ¬p) = (q , contradiction′ ¬p)
+  helper (no ¬p) = (q , λ p → contradiction′ ¬p p)
 
 -- The independence of premise rule for binary sums.
 
@@ -91,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (contradiction′ ¬p)
+  helper (no ¬p) = inj₁ λ p → contradiction′ ¬p p
 
 private
 

src/Relation/Nullary/Negation/Core.agda

@@ -66,20 +66,17 @@ negated-stable ¬¬¬a a = ¬¬¬a (¬¬-η a)
 ------------------------------------------------------------------------
 -- Properties, II: using the *ex falso* rule ⊥-elim
 
-contradiction-irr : .A → .(¬ A) → Whatever
-contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
+contradiction : .A → .(¬ A) → Whatever
+contradiction a ¬a = ⊥-elim-irr (¬a a)
 
-contradiction : A → ¬ A → Whatever
-contradiction a ¬a = contradiction-irr a ¬a
-
-contradiction′ : ¬ A → A → Whatever
-contradiction′ ¬a a = contradiction-irr a ¬a
+contradiction′ : .(¬ A) → .A → Whatever
+contradiction′ ¬a a = ⊥-elim-irr (¬a a)
 
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
 
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
-stable ¬[¬¬a→a] = ¬[¬¬a→a] (contradiction (¬[¬¬a→a] ∘ const))
+stable ¬[¬¬a→a] = ¬[¬¬a→a] λ ¬¬a → contradiction (¬[¬¬a→a] ∘ const) ¬¬a
 

src/Relation/Nullary/Reflects.agda

@@ -18,7 +18,7 @@ open import Data.Empty.Polymorphic using (⊥)
 open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id)
 open import Relation.Nullary.Negation.Core
-  using (¬_; contradiction-irr; contradiction; _¬-⊎_)
+  using (¬_; contradiction; _¬-⊎_)
 open import Relation.Nullary.Recomputable as Recomputable using (Recomputable)
 
 private
@@ -61,7 +61,7 @@ invert (ofⁿ ¬a) = ¬a
 
 recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
-recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
+recompute (ofⁿ ¬a) a = contradiction a ¬a
 
 recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) →
                      recompute r p ≡ recompute r q