Enhancement to Relation.Nullary.Reflects etc.

doc/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-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 {x} {y} x≡y = reflects′ (x ≡ y) id (contradiction x≡y) (proof (x ≟ y))
+
+ ≡-normalise-constant : ∀ {x y} (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
+ ≡-normalise-constant {x} {y} x≡y _
+ = reflects′ _ (λ _ → refl) (contradiction x≡y) (proof (x ≟ y))
 
  ≡-irrelevant : UIP A
  ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant

src/Data/Nat/Properties.agda

@@ -20,7 +20,6 @@ import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
 open import Data.Bool.Base using (Bool; false; true; T)
-open import Data.Bool.Properties using (T?)
 open import Data.Nat.Base
 open import Data.Product.Base using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum
@@ -35,10 +34,10 @@ open import Relation.Binary.Core
 open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary hiding (Irrelevant)
-open import Relation.Nullary.Decidable using (True; via-injection; map′)
+open import Relation.Nullary.Decidable
+ using (Dec; yes; no; T?; True; via-injection; map′)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
-open import Relation.Nullary.Reflects using (fromEquivalence)
+open import Relation.Nullary.Reflects as Reflects using (Reflects)
 
 open import Algebra.Definitions {A = ℕ} _≡_
  hiding (LeftCancellative; RightCancellative; Cancellative)
@@ -135,7 +134,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 <⇒<ᵇ (s<s m<n@(s≤s _)) = <⇒<ᵇ m<n
 
 <ᵇ-reflects-< : ∀ m n → Reflects (m < n) (m <ᵇ n)
-<ᵇ-reflects-< m n = fromEquivalence (<ᵇ⇒< m n) <⇒<ᵇ
+<ᵇ-reflects-< m n = Reflects.fromEquivalence (<ᵇ⇒< m n) <⇒<ᵇ
 
 ------------------------------------------------------------------------
 -- Properties of _≤ᵇ_
@@ -150,7 +149,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≤⇒≤ᵇ m≤n@(s≤s _) = <⇒<ᵇ m≤n
 
 ≤ᵇ-reflects-≤ : ∀ m n → Reflects (m ≤ n) (m ≤ᵇ n)
-≤ᵇ-reflects-≤ m n = fromEquivalence (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ
+≤ᵇ-reflects-≤ m n = Reflects.fromEquivalence (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ
 
 ------------------------------------------------------------------------
 -- Properties of _≤_

src/Relation/Nullary.agda

@@ -25,6 +25,7 @@ private
 
 open import Relation.Nullary.Negation.Core public
 open import Relation.Nullary.Reflects public
+ hiding (recompute; fromEquivalence)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
@@ -35,11 +36,11 @@ Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
 
 ------------------------------------------------------------------------
 -- Recomputability - we can rebuild a relevant proof given an
--- irrelevant one.
-
+-- irrelevant one. NOW moved to Relation.Nullary.Reflects
+{-
 Recomputable : Set p → Set p
 Recomputable P = .P → P
-
+-}
 ------------------------------------------------------------------------
 -- Weak decidability
 -- `nothing` is 'don't know'/'give up'; `just` is `yes`/`definitely`

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.Product.Base using (∃; _,_)
+open import Data.Bool.Base using (true; false; T)
+open import Data.Product.Base using (∃; ∃-syntax; _,_)
 open import Function.Base
 open import Function.Bundles using
- (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
+ (Injection; module Injection; module Equivalence; _⇔_; mk⇔; _↔_; 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; sym; trans; cong′)
 
@@ -32,6 +30,26 @@ private
 
 open import Relation.Nullary.Decidable.Core public
 
+------------------------------------------------------------------------
+-- Characterisation : Dec A ⇔ there exists a Bool b st A ⇔ T b
+
+-- forwards direction: use `does`
+
+dec⇔T∘does : (A? : Dec A) → A ⇔ T (does A?)
+dec⇔T∘does A? = mk⇔ (does-complete A?) (does-sound A?)
+
+dec⇒∃⇔T : (A? : Dec A) → ∃[ b ] A ⇔ T b
+dec⇒∃⇔T A? = does A? , dec⇔T∘does A?
+
+-- backwards direction: inherit from `Decidable.Core`
+∃⇔T⇒dec : (∃[ b ] A ⇔ T b) → Dec A
+∃⇔T⇒dec (b , A⇔Tb) = fromEquivalence from to
+ where open Equivalence A⇔Tb
+
+-- finally
+dec⇔∃⇔T : Dec A ⇔ (∃[ b ] A ⇔ T b)
+dec⇔∃⇔T = mk⇔ dec⇒∃⇔T ∃⇔T⇒dec
+
 ------------------------------------------------------------------------
 -- Maps
 
@@ -52,23 +70,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