Rename and deprecate excluded-middle (#2026)

Author: Saransh-cpp

CHANGELOG.md

@@ -881,7 +881,8 @@ Non-backwards compatible changes
     lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
     lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
     ```
-
+  * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
+    `¬¬-excluded-middle`.
 
 Major improvements
 ------------------

src/Axiom/DoubleNegationElimination.agda

@@ -32,4 +32,4 @@ em⇒dne : ∀ {ℓ} → ExcludedMiddle ℓ → DoubleNegationElimination ℓ
 em⇒dne em = decidable-stable em
 
 dne⇒em : ∀ {ℓ} → DoubleNegationElimination ℓ → ExcludedMiddle ℓ
-dne⇒em dne = dne excluded-middle
+dne⇒em dne = dne ¬¬-excluded-middle

src/Codata/Musical/Colist.agda

@@ -36,7 +36,7 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
 open import Relation.Nullary.Negation
-open import Relation.Nullary.Decidable using (excluded-middle)
+open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
 open import Relation.Unary using (Pred)
 
 private
@@ -244,7 +244,7 @@ not-finite-is-infinite (x ∷ xs) hyp =
 
 finite-or-infinite :
   (xs : Colist A) → ¬ ¬ (Finite xs ⊎ Infinite xs)
-finite-or-infinite xs = helper <$> excluded-middle
+finite-or-infinite xs = helper <$> ¬¬-excluded-middle
   where
   helper : Dec (Finite xs) → Finite xs ⊎ Infinite xs
   helper ( true because  [fin]) = inj₁ (invert [fin])

src/Data/List/Membership/Propositional/Properties.agda

@@ -44,7 +44,7 @@ import Relation.Nullary.Reflects as Reflects
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (¬_; Dec; does; yes; no; _because_)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (excluded-middle)
+open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
@@ -345,7 +345,7 @@ module _ {_•_ : Op₂ A} where
 
 finite : (f : ℕ ↣ A) → ∀ xs → ¬ (∀ i → Injection.to f ⟨$⟩ i ∈ xs)
 finite inj []       fᵢ∈[]   = ¬Any[] (fᵢ∈[] 0)
-finite inj (x ∷ xs) fᵢ∈x∷xs = excluded-middle helper
+finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper
   where
   open Injection inj renaming (injective to f-inj)
 

src/Effect/Monad/Partiality.agda

@@ -401,7 +401,7 @@ module _ {A : Set a} {_∼_ : A → A → Set ℓ} where
   now-or-never : Reflexive _∼_ →
                  ∀ {k} (x : A ⊥) →
                  ¬ ¬ ((∃ λ y → x ⇓[ other k ] y) ⊎ x ⇑[ other k ])
-  now-or-never refl x = helper <$> excluded-middle
+  now-or-never refl x = helper <$> ¬¬-excluded-middle
     where
     open RawMonad ¬¬-Monad
 

src/Relation/Nullary/Decidable/Core.agda

@@ -176,5 +176,13 @@ decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
 -- A double-negation-translated variant of excluded middle (or: every
 -- nullary relation is decidable in the double-negation monad).
 
+¬¬-excluded-middle : DoubleNegation (Dec P)
+¬¬-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
+
 excluded-middle : DoubleNegation (Dec P)
-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
+excluded-middle = ¬¬-excluded-middle
+
+{-# WARNING_ON_USAGE excluded-middle
+"Warning: excluded-middle was deprecated in v2.0.
+Please use ¬¬-excluded-middle instead."
+#-}

src/Relation/Nullary/Negation.agda

@@ -15,7 +15,7 @@ open import Data.Product.Base as Prod using (_,_; Σ; Σ-syntax; ∃; curry; unc
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (flip; _∘_; const; _∘′_)
 open import Level using (Level)
-open import Relation.Nullary.Decidable.Core using (Dec; yes; no; excluded-middle)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; ¬¬-excluded-middle)
 open import Relation.Unary using (Universal)
 
 private
@@ -85,7 +85,7 @@ call/cc hyp ¬p = hyp (λ p → ⊥-elim (¬p p)) ¬p
 
 independence-of-premise : {R : Q → Set r} →
                           Q → (P → Σ Q R) → DoubleNegation (Σ[ x ∈ Q ] (P → R x))
-independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
+independence-of-premise {P = P} q f = ¬¬-map helper ¬¬-excluded-middle
   where
   helper : Dec P → _
   helper (yes p) = Prod.map₂ const (f p)
@@ -94,7 +94,7 @@ independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
 -- The independence of premise rule for binary sums.
 
 independence-of-premise-⊎ : (P → Q ⊎ R) → DoubleNegation ((P → Q) ⊎ (P → R))
-independence-of-premise-⊎ {P = P} f = ¬¬-map helper excluded-middle
+independence-of-premise-⊎ {P = P} f = ¬¬-map helper ¬¬-excluded-middle
   where
   helper : Dec P → _
   helper (yes p) = Sum.map const const (f p)