module Data.Dec.Base where

Decidable typesπŸ”—

The type Dec, of decisions for a type A, is a renaming of the coproduct A ⊎ ¬ A. A value of Dec A witnesses not that A is decidable, but that it has been decided; A witness of decidability, then, is a proof assigning decisions to values of a certain type.

data Dec {β„“} (A : Type β„“) : Type β„“ where
  yes : (a  :   A) β†’ Dec A
  no  : (Β¬a : Β¬ A) β†’ Dec A

Dec-elim
  : βˆ€ {β„“ β„“'} {A : Type β„“} (P : Dec A β†’ Type β„“')
  β†’ (βˆ€ y β†’ P (yes y))
  β†’ (βˆ€ y β†’ P (no y))
  β†’ βˆ€ x β†’ P x
Dec-elim P f g (yes x) = f x
Dec-elim P f g (no x)  = g x

Dec-rec
  : βˆ€ {β„“ β„“'} {A : Type β„“} {X : Type β„“'}
  β†’ (A β†’ X)
  β†’ (Β¬ A β†’ X)
  β†’ Dec A β†’ X
Dec-rec = Dec-elim _

A type is discrete if it has decidable equality.

Discrete : βˆ€ {β„“} β†’ Type β„“ β†’ Type β„“
Discrete A = {x y : A} β†’ Dec (x ≑ y)

If we can construct a pair of maps and then we can deduce decidability of from decidability of 

Dec-map
  : (A β†’ B) β†’ (B β†’ A)
  β†’ Dec A β†’ Dec B
Dec-map to from (yes a) = yes (to a)
Dec-map to from (no ¬a) = no (¬a ∘ from)

Dec-≃ : A ≃ B β†’ Dec A β†’ Dec B
Dec-≃ e = Dec-map (Equiv.to e) (Equiv.from e)

This lets us show the following useful lemma: if injects into a discrete type, then is also discrete.

Discrete-inj
  : (f : A β†’ B)
  β†’ (βˆ€ {x y} β†’ f x ≑ f y β†’ x ≑ y)
  β†’ Discrete B β†’ Discrete A
Discrete-inj f inj eq? {x} {y} =
  Dec-map inj (ap f) (eq? {f x} {f y})

Programming with decisionsπŸ”—

Despite the failure of Dec A to be a proposition for general A, in the 1Lab, we like to work with decisions through instance search. This is facilitated by the following functions, which perform instance search:

-- Searches for a type given explicitly.
holds? : βˆ€ {β„“} (A : Type β„“) ⦃ d : Dec A ⦄ β†’ Dec A
holds? A ⦃ d ⦄ = d

-- Searches for equality of inhabitants of a discrete type.
_≑?_ : ⦃ d : Discrete A ⦄ (x y : A) β†’ Dec (x ≑ y)
x ≑? y = holds? (x ≑ y)

infix 3 _≑?_

And the following operators, which combine instance search with case analysis:

caseᡈ_of_ : βˆ€ {β„“ β„“'} (A : Type β„“) ⦃ d : Dec A ⦄ {B : Type β„“'} β†’ (Dec A β†’ B) β†’ B
caseᡈ A of f = f (holds? A)

caseᡈ_return_of_ : βˆ€ {β„“ β„“'} (A : Type β„“) ⦃ d : Dec A ⦄ (B : Dec A β†’ Type β„“') β†’ (βˆ€ x β†’ B x) β†’ B d
caseᡈ A return P of f = f (holds? A)

{-# INLINE caseᡈ_of_        #-}
{-# INLINE caseᡈ_return_of_ #-}

We then have the following basic instances for combining decisions, expressing that the class of decidable types is closed under products and functions, and contains the unit type and the empty type.

instance
  Dec-Γ— : ⦃ _ : Dec P ⦄ ⦃ _ : Dec Q ⦄ β†’ Dec (P Γ— Q)
  Dec-Γ— {Q = _} ⦃ yes p ⦄ ⦃ yes q ⦄ = yes (p , q)
  Dec-Γ— {Q = _} ⦃ yes p ⦄ ⦃ no Β¬q ⦄ = no Ξ» z β†’ Β¬q (snd z)
  Dec-Γ— {Q = _} ⦃ no Β¬p ⦄ ⦃ _ ⦄     = no Ξ» z β†’ Β¬p (fst z)

  Dec-β†’ : ⦃ _ : Dec P ⦄ ⦃ _ : Dec Q ⦄ β†’ Dec (P β†’ Q)
  Dec-β†’ {Q = _} ⦃ yes p ⦄ ⦃ yes q ⦄ = yes Ξ» _ β†’ q
  Dec-β†’ {Q = _} ⦃ yes p ⦄ ⦃ no Β¬q ⦄ = no Ξ» pq β†’ Β¬q (pq p)
  Dec-β†’ {Q = _} ⦃ no Β¬p ⦄ ⦃ q ⦄ = yes Ξ» p β†’ absurd (Β¬p p)

  Dec-⊀ : Dec ⊀
  Dec-⊀ = yes tt

  Dec-βŠ₯ : Dec βŠ₯
  Dec-βŠ₯ = no id