module Functions.Views.Decidability where

Import List

open import Data.Nat   using (ℕ; zero; suc; pred; _+_; _≤_; s≤s; z≤n; _<_; _>_)
open import Data.Bool  using (Bool; true; false; if_then_else_; not)
open import Data.Unit  using (⊤; tt)
open import Data.Empty using (⊥)
open import Function   using (const; _$_)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; cong)

Definition

The decidability view is a view on Set, a function with type (A : Set) → A ⊎ ¬ A.

Individual constructors

A ⊎ ¬ A ~ Dec A where

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

Discussion

In Agda the decidability view can only be postulated, it cannot be defined.

We do not want to work with postulates, so define the decidability view on the "classical fragment" of Set, case-by-case.

Exercises

Define the decidability view for 1 < 2, 1 ≡ 1, 1 ≡ 2 and 1 > 2:

1<2 : Dec ( < )

1≡1 : Dec ( ≡ )

1≡2 : Dec ( ≡ )

1>2 : Dec ( > )

Exercises

Define the decidability view for n ≡ m and n ≤ m where n m : ℕ:

_≟_ : (a b : ℕ) → Dec (a ≡ b)

_≤?_ : (a b : ℕ) → Dec (a ≤ b)

Usage of the decidability view

• The decidability view turns Agda into a classical environment (otherwise it is constructive).

• Dec P can be seen as an extended Boolean value as the following function shows:

⌊_⌋ : {P : Set} → Dec P → Bool
⌊ yes _ ⌋ = true
⌊ no  _ ⌋ = false