Decidability

1. Decidability

1 Decidability

module Lib.Data.Decidability where

This file defines some notions of decidability for types, and proves some decidability results.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Stdlib.Prelude
import Lib.Data.Coprod
import Lib.Data.Empty
import Lib.Data.Unit
import Lib.Prop.Prod

1.2 Definition

A type A is said decidable if A + (neg A).

is-decidable (A : U) : U = Coprod A (neg A)

A type A has a decidable equality if for all x, y : A, x = y is decidable.

has-decidable-equality (A : U) : U =
  (x y : A) → is-decidable (Path A x y)

1.3 Some results about decidability

1.3.1 Empty is decidable

Indeed, (neg Empty) is Empty \to Empty hence it is populated by the identity.

is-decidable/Empty : is-decidable Empty =
  inr (id Empty)

1.3.2 Unit is decidable

Indeed, star inhabits Unit.

is-decidable/Unit : is-decidable Unit =
  inl star

1.3.3 Any inhabited type is decidable

is-decidable/inhabited-type (A : U) (a : A) : is-decidable A =
  inl a

1.4 Closure under coproducts

It suffices to proceed by coprod-induction on the decidability of A and B. Coproducts behave as an "or", thus it is almost always inl except when we have both neg A and neg B.

is-decidable/Coprod (A B : U) (dA : is-decidable A) (dB : is-decidable B) : is-decidable (Coprod A B) =
  ind-Coprod A (neg A) (λ_. is-decidable (Coprod A B))
            (λa. inl (inl a))
            (λf. ind-Coprod B (neg B) (λ_. is-decidable (Coprod A B))
                            (λb. inl (inr b))
                            (λg. inr (ind-Coprod A B (λ_. Empty) f g)) dB) dA

1.5 Closure under products

It suffices to proceed by coprod-induction on the decidability of A and B. Products behave as an "and", thus, as we expect, we find inl only once and inr otherwise.

is-decidable/Prod (A B : U) (dA : is-decidable A) (dB : is-decidable B) : is-decidable (A * B) =
  ind-Coprod A (neg A) (λ_. is-decidable (A * B))
             (λa. ind-Coprod B (neg B) (λ_. is-decidable (A * B))
                             (λb. inl (a, b))
                             (λg. inr (ind-Prod A B (λ_. Empty) (λ_. g))) dB)
             (λf. inr (ind-Prod A B (λ_. Empty) (λx y. f x))) dA

1.6 Closure under function types

is-decidable/map (A B : U) (dA : is-decidable A) (dB : is-decidable B) : is-decidable (A → B) =
  ind-Coprod A (neg A) (λ_. is-decidable (A → B))
               (λa. ind-Coprod B (neg B) (λ_. is-decidable (A → B))
                               (λb. inl (λx. b))
                               (λg. inr (λh. g (h a))) dB)
               (λf. inl (λa. ex-falso B (f a))) dA

An immediate consequence is that if A is decidable, then neg A is also decidable.

is-decidable/neg (A : U) (d : is-decidable A) : is-decidable (neg A) =
  is-decidable/map A Empty d is-decidable/Empty