------------------------------------------------------------------------
-- Operations on and properties of decidable relations
------------------------------------------------------------------------

module Relation.Nullary.Decidable where

open import Data.Empty
open import Data.Function
open import Data.Bool
open import Data.Product hiding (map)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

decToBool : ∀ {P} → Dec P → Bool
decToBool (yes _) = true
decToBool (no  _) = false

True : ∀ {P} → Dec P → Set
True Q = T (decToBool Q)

False : ∀ {P} → Dec P → Set
False Q = T (not (decToBool Q))

witnessToTruth : ∀ {P} {Q : Dec P} → True Q → P
witnessToTruth {Q = yes p} _  = p
witnessToTruth {Q = no  _} ()

map : ∀ {P Q} → P ⇔ Q → Dec P → Dec Q
map eq (yes p) = yes (proj₁ eq p)
map eq (no ¬p) = no (¬p ∘ proj₂ eq)

fromYes : ∀ {P} → P → Dec P → P
fromYes _ (yes p) = p
fromYes p (no ¬p) = ⊥-elim (¬p p)

fromYes-map-commute :
  ∀ {P Q p q} (eq : P ⇔ Q) (d : Dec P) →
  fromYes q (map eq d) ≡ proj₁ eq (fromYes p d)
fromYes-map-commute         _ (yes p) = refl
fromYes-map-commute {p = p} _ (no ¬p) = ⊥-elim (¬p p)