Enhancement to Relation.Nullary.Reflects etc.

README/Design/Decidability.agda

@@ -31,14 +31,14 @@ infix 4 _≟₀_ _≟₁_ _≟₂_
 -- a proof of `Reflects P false` amounts to a refutation of `P`.
 
 ex₀ : (n : ℕ) → Reflects (n ≡ n) true
-ex₀ n = ofʸ refl
+ex₀ n = of refl
 
 ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false
-ex₁ n = ofⁿ λ ()
+ex₁ n = of λ ()
 
 ex₂ : (b : Bool) → Reflects (T b) b
-ex₂ false = ofⁿ id
-ex₂ true  = ofʸ tt
+ex₂ false = of id
+ex₂ true  = of tt
 
 ------------------------------------------------------------------------
 -- Dec
@@ -85,8 +85,8 @@ zero  ≟₁ suc n = no λ ()
 suc m ≟₁ zero  = no λ ()
 does  (suc m ≟₁ suc n) = does (m ≟₁ n)
 proof (suc m ≟₁ suc n) with m ≟₁ n
-... | yes p = ofʸ (cong suc p)
-... | no ¬p = ofⁿ (¬p ∘ suc-injective)
+... | yes p = of (cong suc p)
+... | no ¬p = of (¬p ∘ suc-injective)
 
 -- We now get definitional equalities such as the following.
 

src/Axiom/UniquenessOfIdentityProofs.agda

@@ -8,23 +8,27 @@
 
 module Axiom.UniquenessOfIdentityProofs where
 
-open import Data.Bool.Base using (true; false)
-open import Data.Empty
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary hiding (Irrelevant)
+open import Function.Base using (id; const; flip)
+open import Level using (Level)
+open import Relation.Nullary using (contradiction; reflects′; proof)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
 
+private
+  variable
+    a : Level
+    A : Set a
+
 ------------------------------------------------------------------------
 -- Definition
 --
 -- Uniqueness of Identity Proofs (UIP) states that all proofs of
 -- equality are themselves equal. In other words, the equality relation
 -- is irrelevant. Here we define UIP relative to a given type.
 
-UIP : ∀ {a} (A : Set a) → Set a
+UIP : (A : Set a) → Set a
 UIP A = Irrelevant {A = A} _≡_
 
 ------------------------------------------------------------------------
@@ -38,12 +42,11 @@ UIP A = Irrelevant {A = A} _≡_
 -- proof to its image via this function which we then know is equal to
 -- the image of any other proof.
 
-module Constant⇒UIP
-  {a} {A : Set a} (f : _≡_ {A = A} ⇒ _≡_)
-  (f-constant : ∀ {a b} (p q : a ≡ b) → f p ≡ f q)
+module Constant⇒UIP (f : _≡_ {A = A} ⇒ _≡_)
+                    (f-constant : ∀ {x y} (p q : x ≡ y) → f p ≡ f q)
   where
 
-  ≡-canonical : ∀ {a b} (p : a ≡ b) → trans (sym (f refl)) (f p) ≡ p
+  ≡-canonical : ∀ {x y} (p : x ≡ y) → trans (sym (f refl)) (f p) ≡ p
   ≡-canonical refl = trans-symˡ (f refl)
 
   ≡-irrelevant : UIP A
@@ -59,19 +62,14 @@ module Constant⇒UIP
 -- function over proofs of equality which is constant: it returns the
 -- proof produced by the decision procedure.
 
-module Decidable⇒UIP
-  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
-  where
+module Decidable⇒UIP (_≟_ : Decidable {A = A} _≡_) where
 
   ≡-normalise : _≡_ {A = A} ⇒ _≡_
-  ≡-normalise {a} {b} a≡b with a ≟ b
-  ... | true  because  [p] = invert [p]
-  ... | false because [¬p] = ⊥-elim (invert [¬p] a≡b)
+  ≡-normalise {a} {b} a≡b = reflects′ id (contradiction a≡b) (proof (a ≟ b))
 
   ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
-  ≡-normalise-constant {a} {b} p q with a ≟ b
-  ... | true  because   _  = refl
-  ... | false because [¬p] = ⊥-elim (invert [¬p] p)
+  ≡-normalise-constant {a} {b} a≡b _
+    = reflects′ (λ _ → refl) (contradiction a≡b) (proof (a ≟ b))
 
   ≡-irrelevant : UIP A
   ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant

src/Relation/Nullary.agda

@@ -21,12 +21,12 @@ open import Relation.Nullary.Negation.Core public using
   )
 
 open import Relation.Nullary.Reflects public using
-  ( Reflects; ofʸ; ofⁿ
+  ( Reflects; ofʸ; ofⁿ; reflects; reflects′; of; invert; Recomputable
   ; _×-reflects_; _⊎-reflects_; _→-reflects_
   )
 
 open import Relation.Nullary.Decidable.Core public using
-  ( Dec; does; proof; yes; no; _because_; recompute
+  ( Dec; _because_; does; proof; yes′; no′; yes; no; recompute
   ; ¬?; _×-dec_; _⊎-dec_; _→-dec_
   )
 

src/Relation/Nullary/Decidable.agda

@@ -9,16 +9,14 @@
 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.Bool.Base using (true; false)
 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.Reflects using (invert)
+open import Relation.Nullary using (invert; ¬_; contradiction; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong′)
 
 private
@@ -51,23 +49,23 @@ via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
 -- A lemma relating True and Dec
 
 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) λ ()
+True-↔ (yes′ [a]) irr = let  a = invert  [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
+True-↔ (no′ [¬a]) _   = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
 
 isYes≗does : (a? : Dec A) → isYes a? ≡ does a?
-isYes≗does (true  because _) = refl
-isYes≗does (false because _) = refl
+isYes≗does (yes′ _) = refl
+isYes≗does (no′  _) = refl
 
 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-true (yes′  _ ) a = refl
+dec-true (no′ [¬a]) a = contradiction a (invert [¬a])
 
 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-false (no′   _ ) ¬a = refl
+dec-false (yes′ [a]) ¬a = contradiction (invert [a]) ¬a
 
 dec-yes : (a? : Dec A) → A → ∃ λ a → a? ≡ yes a
 dec-yes a? a with dec-true a? a

src/Relation/Nullary/Decidable/Core.agda

@@ -12,19 +12,19 @@
 module Relation.Nullary.Decidable.Core where
 
 open import Level using (Level; Lift)
-open import Data.Bool.Base using (Bool; false; true; not; T; _∧_; _∨_)
+open import Data.Bool.Base
 open import Data.Unit.Base using (⊤)
-open import Data.Empty using (⊥)
-open import Data.Empty.Irrelevant using (⊥-elim)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
-open import Relation.Nullary.Reflects
+open import Relation.Nullary.Reflects as Reflects
+  using (Reflects; ofʸ; ofⁿ; of; invert; Recomputable)
 open import Relation.Nullary.Negation.Core
+  using (¬_; contradiction; Stable; DoubleNegation; negated-stable)
 
 private
   variable
-    a b : Level
+    a : Level
     A B : Set a
 
 ------------------------------------------------------------------------
@@ -35,8 +35,8 @@ private
 -- reflects the boolean result. This definition allows the boolean
 -- part of the decision procedure to compute independently from the
 -- proof. This leads to better computational behaviour when we only care
--- about the result and not the proof. See README.Decidability for
--- further details.
+-- about the result and not the proof. See README.Design.Decidability
+-- for further details.
 
 infix 2 _because_
 
@@ -48,30 +48,32 @@ record Dec (A : Set a) : Set a where
 
 open Dec public
 
-pattern yes a =  true because ofʸ  a
-pattern no ¬a = false because ofⁿ ¬a
+-- lazier versions of `yes` and `no`
+pattern yes′ [a] =  true because  [a]
+pattern no′ [¬a] = false because [¬a]
+
+-- now these are derived patterns, but could be re-expressed using `of`
+pattern yes  a  = yes′ (ofʸ a)
+pattern no [¬a] = no′ (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-yes a? = if (does a?) then A else Lift a ⊤
 
   From-no : Dec A → Set a
-  From-no (false because _) = ¬ A
-  From-no (true  because _) = Lift a ⊤
+  From-no  a? = if (does a?) then Lift a ⊤ else ¬ A
 
 ------------------------------------------------------------------------
 -- Recompute
 
 -- Given an irrelevant proof of a decidable type, a proof can
 -- be recomputed and subsequently used in relevant contexts.
 recompute : Dec A → .A → A
-recompute (yes a) _ = a
-recompute (no ¬a) a = ⊥-elim (¬a a)
+recompute = Reflects.recompute ∘ proof
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
@@ -81,19 +83,19 @@ infixr 2 _×-dec_ _→-dec_
 
 ¬? : Dec A → Dec (¬ A)
 does  (¬? a?) = not (does a?)
-proof (¬? a?) = ¬-reflects (proof a?)
+proof (¬? a?) = Reflects.¬-reflects (proof a?)
 
 _×-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?
+proof (a? ×-dec b?) = proof a? Reflects.×-reflects proof b?
 
 _⊎-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?
+proof (a? ⊎-dec b?) = proof a? Reflects.⊎-reflects proof b?
 
 _→-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?
+proof (a? →-dec b?) = proof a? Reflects.→-reflects proof b?
 
 ------------------------------------------------------------------------
 -- Relationship with booleans
@@ -104,8 +106,8 @@ proof (a? →-dec b?) = proof a? →-reflects proof b?
 -- for proof automation.
 
 isYes : Dec A → Bool
-isYes (true  because _) = true
-isYes (false because _) = false
+isYes (yes′ _) = true
+isYes (no′  _) = false
 
 isNo : Dec A → Bool
 isNo = not ∘ isYes
@@ -124,51 +126,51 @@ False = T ∘ isNo
 
 -- Gives a witness to the "truth".
 toWitness : {a? : Dec A} → True a? → A
-toWitness {a? = true  because [a]} _  = invert [a]
-toWitness {a? = false because  _ } ()
+toWitness {a? = yes′ [a]} _ = invert [a]
+toWitness {a? = no′  _ } ()
 
 -- Establishes a "truth", given a witness.
 fromWitness : {a? : Dec A} → A → True a?
-fromWitness {a? = true  because   _ } = const _
-fromWitness {a? = false because [¬a]} = invert [¬a]
+fromWitness {a? = yes′  _ } = const _
+fromWitness {a? = no′ [¬a]} = invert [¬a]
 
 -- Variants for False.
 toWitnessFalse : {a? : Dec A} → False a? → ¬ A
-toWitnessFalse {a? = true  because   _ } ()
-toWitnessFalse {a? = false because [¬a]} _  = invert [¬a]
+toWitnessFalse {a? = yes′  _ } ()
+toWitnessFalse {a? = no′ [¬a]} _  = invert [¬a]
 
 fromWitnessFalse : {a? : Dec A} → ¬ A → False a?
-fromWitnessFalse {a? = true  because [a]} = flip _$_ (invert [a])
-fromWitnessFalse {a? = false because  _ } = const _
+fromWitnessFalse {a? = yes′ [a]} = flip _$_ (invert [a])
+fromWitnessFalse {a? = no′   _ } = const _
 
 -- If a decision procedure returns "yes", then we can extract the
 -- proof using from-yes.
 from-yes : (a? : Dec A) → From-yes a?
-from-yes (true  because [a]) = invert [a]
-from-yes (false because _ ) = _
+from-yes (yes′ [a]) = invert [a]
+from-yes (no′   _ ) = _
 
 -- If a decision procedure returns "no", then we can extract the proof
 -- using from-no.
 from-no : (a? : Dec A) → From-no a?
-from-no (false because [¬a]) = invert [¬a]
-from-no (true  because   _ ) = _
+from-no (no′ [¬a]) = invert [¬a]
+from-no (yes′  _ ) = _
 
 ------------------------------------------------------------------------
 -- Maps
 
 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)
+does  (map′ A→B B→A a?)        = does a?
+proof (map′ A→B B→A (yes′ [a])) = of (A→B (invert [a]))
+proof (map′ A→B B→A (no′ [¬a])) = of (invert [¬a] ∘ B→A)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation
 
 -- Decidable predicates are stable.
 
 decidable-stable : Dec A → Stable A
-decidable-stable (yes a) ¬¬a = a
-decidable-stable (no ¬a) ¬¬a = ⊥-elim (¬¬a ¬a)
+decidable-stable (yes′ [a]) ¬¬a = invert [a]
+decidable-stable (no′ [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
 ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)