From ddeb9543bb0675b6d0b15ee3d1999224336270a2 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Tue, 20 Jun 2023 10:53:06 -0400 Subject: [PATCH 1/4] =?UTF-8?q?Rename=20`excluded-middle`=20to=20`=C2=AC?= =?UTF-8?q?=C2=AC-excluded-middle`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 3 ++- src/Axiom/DoubleNegationElimination.agda | 2 +- src/Codata/Musical/Colist.agda | 4 ++-- src/Data/List/Membership/Propositional/Properties.agda | 4 ++-- src/Effect/Monad/Partiality.agda | 2 +- src/Relation/Nullary/Decidable/Core.agda | 4 ++-- src/Relation/Nullary/Negation.agda | 4 ++-- 7 files changed, 12 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5891740538..51f5a3aca7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -874,7 +874,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 ------------------ diff --git a/src/Axiom/DoubleNegationElimination.agda b/src/Axiom/DoubleNegationElimination.agda index 49e8b01eaa..777f08c017 100644 --- a/src/Axiom/DoubleNegationElimination.agda +++ b/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 diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda index 2ec01be70f..d70a101f6a 100644 --- a/src/Codata/Musical/Colist.agda +++ b/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]) diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda index 364c6d29b8..2ddd26e02b 100644 --- a/src/Data/List/Membership/Propositional/Properties.agda +++ b/src/Data/List/Membership/Propositional/Properties.agda @@ -43,7 +43,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 {ℓ = ℓ}) @@ -344,7 +344,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) diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda index 0751cb5b15..db412f4add 100644 --- a/src/Effect/Monad/Partiality.agda +++ b/src/Effect/Monad/Partiality.agda @@ -395,7 +395,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 diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index e06dc32239..aee91a6478 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -175,5 +175,5 @@ 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))) diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda index 5111db897f..1b4ddedd0b 100644 --- a/src/Relation/Nullary/Negation.agda +++ b/src/Relation/Nullary/Negation.agda @@ -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) From 1d16c2b5b2118a5ed98007c180918d86e279eeac Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 20 Jul 2023 19:12:41 -0400 Subject: [PATCH 2/4] Add deprecation warning --- src/Relation/Nullary/Decidable/Core.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index aee91a6478..1a29930bce 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -177,3 +177,8 @@ decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p) ¬¬-excluded-middle : DoubleNegation (Dec P) ¬¬-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p))) + +{-# WARNING_ON_USAGE map-identity +"Warning: excluded-middle was deprecated in v2.0. +Please use ¬¬-excluded-middle instead." +#-} From 7cb7c990767bf92cb2232215a40fa9ed326f005a Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 20 Jul 2023 19:33:52 -0400 Subject: [PATCH 3/4] Fix tests --- src/Relation/Nullary/Decidable/Core.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda index 1a29930bce..6296db24df 100644 --- a/src/Relation/Nullary/Decidable/Core.agda +++ b/src/Relation/Nullary/Decidable/Core.agda @@ -178,7 +178,10 @@ decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p) ¬¬-excluded-middle : DoubleNegation (Dec P) ¬¬-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p))) -{-# WARNING_ON_USAGE map-identity +excluded-middle : DoubleNegation (Dec P) +excluded-middle = ¬¬-excluded-middle + +{-# WARNING_ON_USAGE excluded-middle "Warning: excluded-middle was deprecated in v2.0. Please use ¬¬-excluded-middle instead." #-} From af4a82a7eb30e3166f7bbec1868bc608b7036998 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Thu, 20 Jul 2023 20:11:50 -0400 Subject: [PATCH 4/4] Oops, fix import --- src/Relation/Nullary/Negation.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda index 1b4ddedd0b..59e96f3429 100644 --- a/src/Relation/Nullary/Negation.agda +++ b/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