-- The Agda standard library
-- Operations on and properties of decidable relations

{-# OPTIONS --cubical-compatible --safe #-}

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 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.Binary.PropositionalEquality.Core using (_≡_; refl; cong′)

    a b ℓ₁ ℓ₂ : Level
    A B : Set a

-- Re-exporting the core definitions

open import Relation.Nullary.Decidable.Core public

-- Maps

map : A  B  Dec A  Dec B
map A⇔B = map′ to from
  where open Equivalence A⇔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 : {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-↔ : (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 : (a? : Dec A)  isYes a?  does a?
isYes≗does (true  because _) = refl
isYes≗does (false because _) = 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-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 : (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 : (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 : (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