Core.agda

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

open import Agda.Builtin.Equality using (_≡_)
open import Level using (Level; Lift)
open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Data.Product.Base using (_×_)
open import Data.Sum.Base using (_⊎_)
open import Function.Base using (_∘_; const; _$_; flip)
open import Relation.Nullary.Recomputable as Recomputable hiding (recompute-constant)
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

------------------------------------------------------------------------
-- 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 → 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?) = 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 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."
#-}