Modernise Relation.Nullary code (#2110)

Author: MatthewDaggitt

CHANGELOG.md

@@ -1555,6 +1555,11 @@ Deprecated names
   invPreorder   ↦ converse-preorder
   ```
 
+* In `Relation.Nullary.Decidable.Core`:
+  ```
+  excluded-middle  ↦  ¬¬-excluded-middle
+  ```
+
 ### Renamed Data.Erased to Data.Irrelevant
 
 * This fixes the fact we had picked the wrong name originally. The erased modality

src/Codata/Musical/Colist.agda

@@ -67,8 +67,8 @@ take (suc n) []       = Vec≤.[]
 take (suc n) (x ∷ xs) = x Vec≤.∷ take n (♭ xs)
 
 
-module ¬¬Monad {p} where
-  open RawMonad (¬¬-Monad {p}) public
+module ¬¬Monad {a} where
+  open RawMonad (¬¬-Monad {a}) public
 open ¬¬Monad  -- we don't want the RawMonad content to be opened publicly
 
 ------------------------------------------------------------------------

src/Data/Nat/InfinitelyOften.agda

@@ -20,7 +20,8 @@ open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
 open import Relation.Unary using (Pred; _∪_; _⊆_)
-open RawMonad (¬¬-Monad {p = 0ℓ})
+
+open RawMonad (¬¬-Monad {a = 0ℓ})
 
 private
   variable

src/Relation/Nullary/Decidable.agda

@@ -11,22 +11,20 @@ module Relation.Nullary.Decidable where
 open import Level using (Level)
 open import Data.Bool.Base using (true; false; if_then_else_)
 open import Data.Empty using (⊥-elim)
-open import Data.Product.Base as Prod hiding (map)
-open import Data.Sum.Base as Sum hiding (map)
+open import Data.Product.Base using (∃; _,_)
 open import Function.Base
 open import Function.Bundles using
   (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary
-open import Relation.Nullary.Negation
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong′)
 
 private
   variable
-    p q r : Level
-    P Q R : Set p
+    a b ℓ₁ ℓ₂ : Level
+    A B : Set a
 
 ------------------------------------------------------------------------
 -- Re-exporting the core definitions
@@ -36,56 +34,49 @@ open import Relation.Nullary.Decidable.Core public
 ------------------------------------------------------------------------
 -- Maps
 
-map : P ⇔ Q → Dec P → Dec Q
-map P⇔Q = map′ to from
-  where open Equivalence P⇔Q
+map : A ⇔ B → Dec A → Dec B
+map A⇔B = map′ to from
+  where open Equivalence A⇔B
 
-module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
-         (inj : Injection A B)
-  where
-
-  open Injection inj
-  open Setoid A using () renaming (_≈_ to _≈A_)
-  open Setoid B using () renaming (_≈_ to _≈B_)
-
-  -- If there is an injection from one setoid to another, and the
-  -- latter's equivalence relation is decidable, then the former's
-  -- equivalence relation is also decidable.
-
-  via-injection : Decidable _≈B_ → Decidable _≈A_
-  via-injection dec x y =
-    map′ injective cong (dec (to x) (to y))
+-- If there is an injection from one setoid to another, and the
+-- latter's equivalence relation is decidable, then the former's
+-- equivalence relation is also decidable.
+via-injection : {S : Setoid a ℓ₁} {T : Setoid b ℓ₂}
+                (inj : Injection S T) (open Injection inj) →
+                Decidable Eq₂._≈_ → Decidable Eq₁._≈_
+via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
+  where open Injection inj
 
 ------------------------------------------------------------------------
 -- A lemma relating True and Dec
 
-True-↔ : (dec : Dec P) → Irrelevant P → True dec ↔ P
-True-↔ (true  because  [p]) irr = mk↔ₛ′ (λ _ → invert [p]) _ (irr (invert [p])) cong′
-True-↔ (false because ofⁿ ¬p) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬p)) (⊥-elim ∘ ¬p) λ ()
+True-↔ : (a? : Dec A) → Irrelevant A → True a? ↔ A
+True-↔ (true  because [a]) irr = mk↔ₛ′ (λ _ → invert [a]) _ (irr (invert [a])) cong′
+True-↔ (false because ofⁿ ¬a) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬a)) (⊥-elim ∘ ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
 
-isYes≗does : (P? : Dec P) → isYes P? ≡ does P?
+isYes≗does : (a? : Dec A) → isYes a? ≡ does a?
 isYes≗does (true  because _) = refl
 isYes≗does (false because _) = refl
 
-dec-true : (p? : Dec P) → P → does p? ≡ true
-dec-true (true  because   _ ) p = refl
-dec-true (false because [¬p]) p = ⊥-elim (invert [¬p] p)
+dec-true : (a? : Dec A) → A → does a? ≡ true
+dec-true (true  because   _ ) a = refl
+dec-true (false because [¬a]) a = ⊥-elim (invert [¬a] a)
 
-dec-false : (p? : Dec P) → ¬ P → does p? ≡ false
-dec-false (false because  _ ) ¬p = refl
-dec-false (true  because [p]) ¬p = ⊥-elim (¬p (invert [p]))
+dec-false : (a? : Dec A) → ¬ A → does a? ≡ false
+dec-false (false because  _ ) ¬a = refl
+dec-false (true  because [a]) ¬a = ⊥-elim (¬a (invert [a]))
 
-dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
-dec-yes p? p with dec-true p? p
-dec-yes (yes p′) p | refl = p′ , refl
+dec-yes : (a? : Dec A) → A → ∃ λ a → a? ≡ yes a
+dec-yes a? a with dec-true a? a
+dec-yes (yes a′) a | refl = a′ , refl
 
-dec-no : (p? : Dec P) (¬p : ¬ P) → p? ≡ no ¬p
-dec-no p? ¬p with dec-false p? ¬p
+dec-no : (a? : Dec A) (¬a : ¬ A) → a? ≡ no ¬a
+dec-no a? ¬a with dec-false a? ¬a
 dec-no (no _) _ | refl = refl
 
-dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
-dec-yes-irr p? irr p with dec-yes p? p
-... | p′ , eq rewrite irr p p′ = eq
+dec-yes-irr : (a? : Dec A) → Irrelevant A → (a : A) → a? ≡ yes a
+dec-yes-irr a? irr a with dec-yes a? a
+... | a′ , eq rewrite irr a a′ = eq

src/Relation/Nullary/Decidable/Core.agda

@@ -24,9 +24,8 @@ open import Relation.Nullary.Negation.Core
 
 private
   variable
-    p q : Level
-    P : Set p
-    Q : Set q
+    a b : Level
+    A B : Set a
 
 ------------------------------------------------------------------------
 -- Definition.
@@ -41,68 +40,81 @@ private
 
 infix 2 _because_
 
-record Dec {p} (P : Set p) : Set p where
+record Dec (A : Set a) : Set a where
   constructor _because_
   field
     does  : Bool
-    proof : Reflects P does
+    proof : Reflects A does
 
 open Dec public
 
-pattern yes p =  true because ofʸ  p
-pattern no ¬p = false because ofⁿ ¬p
+pattern yes a =  true because ofʸ  a
+pattern no ¬a = false because ofⁿ ¬a
+
+------------------------------------------------------------------------
+-- Flattening
+
+module _ {A : Set a} where
+
+  From-yes : Dec A → Set a
+  From-yes (true  because _) = A
+  From-yes (false because _) = Lift a ⊤
+
+  From-no : Dec A → Set a
+  From-no (false because _) = ¬ A
+  From-no (true  because _) = Lift a ⊤
 
 ------------------------------------------------------------------------
 -- Recompute
 
 -- Given an irrelevant proof of a decidable type, a proof can
 -- be recomputed and subsequently used in relevant contexts.
-recompute : ∀ {a} {A : Set a} → Dec A → .A → A
-recompute (yes x) _ = x
-recompute (no ¬p) x = ⊥-elim (¬p x)
+recompute : Dec A → .A → A
+recompute (yes a) _ = a
+recompute (no ¬a) a = ⊥-elim (¬a a)
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
 
 infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
-¬? : Dec P → Dec (¬ P)
-does  (¬? p?) = not (does p?)
-proof (¬? p?) = ¬-reflects (proof p?)
+¬? : Dec A → Dec (¬ A)
+does  (¬? a?) = not (does a?)
+proof (¬? a?) = ¬-reflects (proof a?)
 
-_×-dec_ : Dec P → Dec Q → Dec (P × Q)
-does  (p? ×-dec q?) = does p? ∧ does q?
-proof (p? ×-dec q?) = proof p? ×-reflects proof q?
+_×-dec_ : Dec A → Dec B → Dec (A × B)
+does  (a? ×-dec b?) = does a? ∧ does b?
+proof (a? ×-dec b?) = proof a? ×-reflects proof b?
 
-_⊎-dec_ : Dec P → Dec Q → Dec (P ⊎ Q)
-does  (p? ⊎-dec q?) = does p? ∨ does q?
-proof (p? ⊎-dec q?) = proof p? ⊎-reflects proof q?
+_⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B)
+does  (a? ⊎-dec b?) = does a? ∨ does b?
+proof (a? ⊎-dec b?) = proof a? ⊎-reflects proof b?
 
-_→-dec_ : Dec P → Dec Q → Dec (P → Q)
-does  (p? →-dec q?) = not (does p?) ∨ does q?
-proof (p? →-dec q?) = proof p? →-reflects proof q?
+_→-dec_ : Dec A → Dec B → Dec (A → B)
+does  (a? →-dec b?) = not (does a?) ∨ does b?
+proof (a? →-dec b?) = proof a? →-reflects proof b?
 
 ------------------------------------------------------------------------
 -- Relationship with booleans
 
 -- `isYes` is a stricter version of `does`. The lack of computation
--- means that we can recover the proposition `P` from `isYes P?` by
+-- means that we can recover the proposition `P` from `isYes a?` by
 -- unification. This is useful when we are using the decision procedure
 -- for proof automation.
 
-isYes : Dec P → Bool
+isYes : Dec A → Bool
 isYes (true  because _) = true
 isYes (false because _) = false
 
-isNo : Dec P → Bool
+isNo : Dec A → Bool
 isNo = not ∘ isYes
 
-True : Dec P → Set
-True Q = T (isYes Q)
+True : Dec A → Set
+True = T ∘ isYes
 
-False : Dec P → Set
-False Q = T (isNo Q)
+False : Dec A → Set
+False = T ∘ isNo
 
 -- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence.
 ⌊_⌋ = isYes
@@ -111,77 +123,72 @@ False Q = T (isNo Q)
 -- Witnesses
 
 -- Gives a witness to the "truth".
-toWitness : {Q : Dec P} → True Q → P
-toWitness {Q = true  because [p]} _  = invert [p]
-toWitness {Q = false because  _ } ()
+toWitness : {a? : Dec A} → True a? → A
+toWitness {a? = true  because [a]} _  = invert [a]
+toWitness {a? = false because  _ } ()
 
 -- Establishes a "truth", given a witness.
-fromWitness : {Q : Dec P} → P → True Q
-fromWitness {Q = true  because   _ } = const _
-fromWitness {Q = false because [¬p]} = invert [¬p]
+fromWitness : {a? : Dec A} → A → True a?
+fromWitness {a? = true  because   _ } = const _
+fromWitness {a? = false because [¬a]} = invert [¬a]
 
 -- Variants for False.
-toWitnessFalse : {Q : Dec P} → False Q → ¬ P
-toWitnessFalse {Q = true  because   _ } ()
-toWitnessFalse {Q = false because [¬p]} _  = invert [¬p]
-
-fromWitnessFalse : {Q : Dec P} → ¬ P → False Q
-fromWitnessFalse {Q = true  because [p]} = flip _$_ (invert [p])
-fromWitnessFalse {Q = false because  _ } = const _
+toWitnessFalse : {a? : Dec A} → False a? → ¬ A
+toWitnessFalse {a? = true  because   _ } ()
+toWitnessFalse {a? = false because [¬a]} _  = invert [¬a]
 
-module _ {p} {P : Set p} where
+fromWitnessFalse : {a? : Dec A} → ¬ A → False a?
+fromWitnessFalse {a? = true  because [a]} = flip _$_ (invert [a])
+fromWitnessFalse {a? = false because  _ } = const _
 
 -- If a decision procedure returns "yes", then we can extract the
 -- proof using from-yes.
-
-  From-yes : Dec P → Set p
-  From-yes (true  because _) = P
-  From-yes (false because _) = Lift p ⊤
-
-  from-yes : (p : Dec P) → From-yes p
-  from-yes (true  because [p]) = invert [p]
-  from-yes (false because _ ) = _
+from-yes : (a? : Dec A) → From-yes a?
+from-yes (true  because [a]) = invert [a]
+from-yes (false because _ ) = _
 
 -- If a decision procedure returns "no", then we can extract the proof
 -- using from-no.
-
-  From-no : Dec P → Set p
-  From-no (false because _) = ¬ P
-  From-no (true  because _) = Lift p ⊤
-
-  from-no : (p : Dec P) → From-no p
-  from-no (false because [¬p]) = invert [¬p]
-  from-no (true  because   _ ) = _
+from-no : (a? : Dec A) → From-no a?
+from-no (false because [¬a]) = invert [¬a]
+from-no (true  because   _ ) = _
 
 ------------------------------------------------------------------------
 -- Maps
 
-map′ : (P → Q) → (Q → P) → Dec P → Dec Q
-does  (map′ P→Q Q→P p?)                   = does p?
-proof (map′ P→Q Q→P (true  because  [p])) = ofʸ (P→Q (invert [p]))
-proof (map′ P→Q Q→P (false because [¬p])) = ofⁿ (invert [¬p] ∘ Q→P)
+map′ : (A → B) → (B → A) → Dec A → Dec B
+does  (map′ A→B B→A a?)                   = does a?
+proof (map′ A→B B→A (true  because  [a])) = ofʸ (A→B (invert [a]))
+proof (map′ A→B B→A (false because [¬a])) = ofⁿ (invert [¬a] ∘ B→A)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation
 
 -- Decidable predicates are stable.
 
-decidable-stable : Dec P → Stable P
-decidable-stable (yes p) ¬¬p = p
-decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
+decidable-stable : Dec A → Stable A
+decidable-stable (yes a) ¬¬a = a
+decidable-stable (no ¬a) ¬¬a = ⊥-elim (¬¬a ¬a)
 
-¬-drop-Dec : Dec (¬ ¬ P) → Dec (¬ P)
-¬-drop-Dec ¬¬p? = map′ negated-stable contradiction (¬? ¬¬p?)
+¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
+¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
 
 -- 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 A)
+¬¬-excluded-middle ¬?a = ¬?a (no (λ a → ¬?a (yes a)))
 
-excluded-middle : DoubleNegation (Dec P)
-excluded-middle = ¬¬-excluded-middle
 
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+excluded-middle = ¬¬-excluded-middle
 {-# WARNING_ON_USAGE excluded-middle
 "Warning: excluded-middle was deprecated in v2.0.
 Please use ¬¬-excluded-middle instead."