open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Sum.Base

open import Meta.Invariant
open import Meta.Idiom

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 _

recover : β {β} {A : Type β} β¦ d : Dec A β¦ β .A β A
recover β¦ yes x β¦ _ = x
recover β¦ no Β¬x β¦ x = absurd (Β¬x x)

decβdne : β {β} {A : Type β} β¦ d : Dec A β¦ β Β¬ Β¬ A β A
decβdne β¦ yes x β¦ _   = x
decβdne β¦ no Β¬x β¦ Β¬Β¬x = absurd (Β¬Β¬x Β¬x)


A type is discrete if it has decidable equality.

Discrete : β {β} β Type β β Type β
Discrete A = {x y : A} β Dec (x β‘ y)

private variable
β β' : Level
A B : Type β


If we can construct a pair of maps and then we can deduce decidability of from decidability of that is, Dec is an Invariant functor.

instance
Invariant-Dec : Invariant (eff Dec)
Invariant-Dec .Invariant.invmap f g (yes a) = yes (f a)
Invariant-Dec .Invariant.invmap f g (no Β¬a) = no (Β¬a β g)


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} =
invmap 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_ #-}

private variable
P Q : Type β


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

instance
Dec-β : β¦ _ : Dec A β¦ β¦ _ : Dec B β¦ β Dec (A β B)
Dec-β β¦ yes A β¦ β¦ _ β¦ = yes (inl A)
Dec-β β¦ no Β¬A β¦ β¦ yes B β¦ = yes (inr B)
Dec-β β¦ no Β¬A β¦ β¦ no Β¬B β¦ = no [ Β¬A , Β¬B ]

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

Dec-Lift : β {β β'} {A : Type β} β β¦ Dec A β¦ β Dec (Lift β' A)
Dec-Lift β¦ d β¦ = Lift-β eβ»ΒΉ <β> d


These closure properties make Dec a Monoidal and Alternative functor.

instance
Monoidal-Dec : Monoidal (eff Dec)
Monoidal-Dec .Monoidal.munit = Dec-β€
Monoidal-Dec .Monoidal._<,>_ a b = Dec-Γ β¦ a β¦ β¦ b β¦

Alternative-Dec : Alternative (eff Dec)
Alternative-Dec .Alternative.empty = Dec-β₯
Alternative-Dec .Alternative._<+>_ a b = Dec-β β¦ a β¦ β¦ b β¦

infix 0 ifα΅_then_else_

ifα΅_then_else_ : Dec A β B β B β B
ifα΅ yes a then y else n = y
ifα΅ no Β¬a then y else n = n

is-yes : β {β} {A : Type β} β Dec A β Type
is-yes (yes x) = β€
is-yes (no _)  = β₯

decide! : β {β} {A : Type β} β¦ d : Dec A β¦ {_ : is-yes d} β A
decide! β¦ yes x β¦ = x


## Relation to sumsπ

The decidability of can also be phrased as so we provide helpers to convert between the two.

from-dec : Dec A β A β Β¬ A
from-dec (yes a) = inl a
from-dec (no Β¬a) = inr Β¬a

to-dec : A β Β¬ A β Dec A
to-dec (inl  a) = yes a
to-dec (inr Β¬a) = no Β¬a


The proof that these functions are inverses is automatic by computation, and thus it can be shown they are equivalences:

from-dec-is-equiv : {A : Type β} β is-equiv (from-dec {A = A})
from-dec-is-equiv = is-isoβis-equiv (iso to-dec p q) where
p : _
p (inl x)  = refl
p (inr Β¬x) = refl

q : _
q (yes x) = refl
q (no x)  = refl

DecβBool : β {A : Type β} β Dec A β Bool
DecβBool (yes x) = true
DecβBool (no Β¬x) = false