    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Operations on and properties of decidable relations
    --
    -- This file contains some core definitions which are re-exported by
    -- Relation.Nullary.Decidable
    ------------------------------------------------------------------------

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

    module Relation.Nullary.Decidable.Core where

    -- decToMaybe was deprecated in v2.1 #2330/#2336
    -- this can go through `Data.Maybe.Base` once that deprecation is fully done.
    open import Agda.Builtin.Equality using (_≡_)
    open import Agda.Builtin.Maybe using (Maybe; just; nothing)
    open import Level using (Level)
    open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
    open import Data.Unit.Polymorphic.Base using (⊤)
    open import Data.Empty.Polymorphic using (⊥)
    open import Data.Product.Base using (_×_)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
    open import Function.Base using (_∘_; const; _$_; flip)
    open import Relation.Nullary.Irrelevant using (Irrelevant)
    open import Relation.Nullary.Recomputable.Core as Recomputable
      using (Recomputable)
    open import Relation.Nullary.Reflects as Reflects
      hiding (recompute; recompute-constant)
    open import Relation.Nullary.Negation.Core
      using (¬_; Stable; negated-stable; contradiction; DoubleNegation)

    private
      variable
        a b : Level
        A B : Set a

    ------------------------------------------------------------------------
    -- Definition.

    -- Decidability proofs have two parts: the `does` term which contains
    -- the boolean result and the `proof` term which contains a proof that
    -- 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.Design.Decidability
    -- for further details.

    infix 2 _because_

    record Dec (A : Set a) : Set a where
      constructor _because_
      field
        does  : Bool
        proof : Reflects A does

    open Dec public

    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 _) = ⊤

      From-no : Dec A → Set a
      From-no (false because _) = ¬ A
      From-no (true  because _) = ⊤

    ------------------------------------------------------------------------
    -- Recompute

    -- Given an irrelevant proof of a decidable type, a proof can
    -- be recomputed and subsequently used in relevant contexts.

    recompute : Dec A → Recomputable A
    recompute = Reflects.recompute ∘ proof

    recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
    recompute-constant = Recomputable.recompute-constant ∘ recompute

    recompute-irrelevant-id : (a? : Dec A) → Irrelevant A → (a : A) → recompute a? a ≡ a
    recompute-irrelevant-id = Recomputable.recompute-irrelevant-id ∘ recompute

    ------------------------------------------------------------------------
    -- Interaction with negation, sum, product etc.

    infixr 1 _⊎-dec_
    infixr 2 _×-dec_ _→-dec_

    T? : ∀ x → Dec (T x)
    T? x = x because T-reflects x

    ¬? : Dec A → Dec (¬ A)
    does  (¬? a?) = not (does a?)
    proof (¬? a?) = ¬-reflects (proof a?)

    ⊤-dec : Dec {a} ⊤
    does  ⊤-dec = true
    proof ⊤-dec = ⊤-reflects

    _×-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 {a} ⊥
    does  ⊥-dec  = false
    proof ⊥-dec  = ⊥-reflects

    _⊎-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 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 Maybe

    dec⇒maybe : Dec A → Maybe A
    dec⇒maybe ( true because [a]) = just (invert [a])
    dec⇒maybe (false because  _ ) = nothing

    ------------------------------------------------------------------------
    -- Relationship with Sum

    toSum : Dec A → A ⊎ ¬ A
    toSum ( true because  [p]) = inj₁ (invert  [p])
    toSum (false because [¬p]) = inj₂ (invert [¬p])

    fromSum : A ⊎ ¬ A → Dec A
    fromSum (inj₁ p)  = yes p
    fromSum (inj₂ ¬p) = no ¬p

    ------------------------------------------------------------------------
    -- Relationship with booleans

    -- `isYes` is a stricter version of `does`. The lack of computation
    -- 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 A → Bool
    isYes (true  because _) = true
    isYes (false because _) = false

    isNo : Dec A → Bool
    isNo = not ∘ isYes

    True : Dec A → Set
    True = T ∘ isYes

    False : Dec A → Set
    False = T ∘ isNo

    -- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence.
    ⌊_⌋ = isYes

    ------------------------------------------------------------------------
    -- Witnesses

    -- Gives a witness to the "truth".
    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 : {a? : Dec A} → A → True a?
    fromWitness {a? = true  because   _ } = const _
    fromWitness {a? = false because [¬a]} = invert [¬a]

    -- Variants for False.
    toWitnessFalse : {a? : Dec A} → False a? → ¬ A
    toWitnessFalse {a? = true  because   _ } ()
    toWitnessFalse {a? = false because [¬a]} _  = invert [¬a]

    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 : (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 : (a? : Dec A) → From-no a?
    from-no (false because [¬a]) = invert [¬a]
    from-no (true  because   _ ) = _

    ------------------------------------------------------------------------
    -- 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)

    ------------------------------------------------------------------------
    -- Relationship with double-negation

    -- Decidable predicates are stable.

    decidable-stable : Dec A → Stable A
    decidable-stable (true  because  [a]) ¬¬a = invert [a]
    decidable-stable (false because [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a

    ¬-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 A)
    ¬¬-excluded-middle ¬?a = ¬?a (no (λ a → ¬?a (yes a)))

    ------------------------------------------------------------------------
    -- 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."
    #-}

    -- Version 2.1

    decToMaybe = dec⇒maybe
    {-# WARNING_ON_USAGE decToMaybe
    "Warning: decToMaybe was deprecated in v2.1.
    Please use Relation.Nullary.Decidable.Core.dec⇒maybe instead."
    #-}

    fromDec = toSum
    {-# WARNING_ON_USAGE fromDec
    "Warning: fromDec was deprecated in v2.1.
    Please use Relation.Nullary.Decidable.Core.toSum instead."
    #-}

    toDec = fromSum
    {-# WARNING_ON_USAGE toDec
    "Warning: toDec was deprecated in v2.1.
    Please use Relation.Nullary.Decidable.Core.fromSum instead."
    #-}