module Functions.Views.Decidability where

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)

The *decidability view* is a view on `Set`

, a function with type `(A : Set) → A ⊎ ¬ A`

.

`A ⊎ ¬ A`

~ `Dec A`

where

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

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.

Define the decidability view for `1 < 2`

, `1 ≡ 1`

, `1 ≡ 2`

and `1 > 2`

:

1<2 : Dec (1 < 2)

1≡1 : Dec (1 ≡ 1)

1≡2 : Dec (1 ≡ 2)

1>2 : Dec (1 > 2)

Define the decidability view for `n ≡ m`

and `n ≤ m`

where `n m : ℕ`

:

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

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

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