Programming Language Foundations in Agda: Decidable

Decidable.agda

module Decidable where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; cong; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _∸_)
open import Data.Product using (_×_; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)

-- https://gist.github.com/pedrominicz/1e85c4ab834a01e990f3e7bc3129e9a0
open import Relations using (_<_; z<s; s<s)

-- https://gist.github.com/pedrominicz/bce9bcfc44f55c04ee5e0b6d903f5809
open import Isomorphism using (_⇔_)

infix 4 _≤_

data _≤_ : ℕ → ℕ → Set where
    z≤n : ∀ {n : ℕ} → zero ≤ n
    s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

data Bool : Set where
    true  : Bool
    false : Bool

infix 4 _≤ᵇ_

_≤ᵇ_ : ℕ → ℕ → Bool
zero  ≤ᵇ n     = true
suc m ≤ᵇ zero  = false
suc m ≤ᵇ suc n = m ≤ᵇ n

T : Bool → Set
T true  = ⊤
T false = ⊥

T→≡ : ∀ (b : Bool) → T b → b ≡ true
T→≡ true tt = refl
T→≡ false ()

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl = tt

≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n
≤ᵇ→≤ zero    n       tt = z≤n
≤ᵇ→≤ (suc m) (suc n) t  = s≤s (≤ᵇ→≤ m n t)

≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)
≤→≤ᵇ z≤n       = tt
≤→≤ᵇ (s≤s m≤n) = ≤→≤ᵇ m≤n

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

¬s≤z : ∀ {n : ℕ} → ¬ (suc n ≤ zero)
¬s≤z ()

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s ¬m≤n (s≤s m≤n) = ¬m≤n m≤n

_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
zero  ≤? n     = yes z≤n
suc m ≤? zero  = no ¬s≤z
suc m ≤? suc n with m ≤? n
...               | yes m≤n = yes (s≤s m≤n)
...               | no ¬m≤n = no (¬s≤s ¬m≤n)

¬n<z : ∀ {n : ℕ} → ¬ (n < zero)
¬n<z ()

¬s<s : ∀ {m n : ℕ} → ¬ (m < n) → ¬ (suc m < suc n)
¬s<s ¬m<n (s<s m<n) = ¬m<n m<n

_<?_ : ∀ (m n : ℕ) → Dec (m < n)
zero  <? suc n = yes z<s
m     <? zero  = no ¬n<z
suc m <? suc n with m <? n
...               | yes m<n = yes (s<s m<n)
...               | no ¬m<n = no (¬s<s ¬m<n)

s≢z : ∀ {n : ℕ} → suc n ≢ zero
s≢z ()

z≢s : ∀ {n : ℕ} → zero ≢ suc n
z≢s ()

s≢s : ∀ {m n : ℕ} → m ≢ n → suc m ≢ suc n
s≢s m≢n m≡n = m≢n (cong (λ x → x ∸ 1) m≡n)

_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
zero  ≡ℕ? zero  = yes refl
suc m ≡ℕ? zero  = no s≢z
zero  ≡ℕ? suc n = no z≢s
suc m ≡ℕ? suc n with m ≡ℕ? n
...                | yes m≡n = yes (cong suc m≡n)
...                | no m≢n  = no (s≢s m≢n)

_≤?'_ : ∀ (m n : ℕ) → Dec (m ≤ n)
m ≤?' n with m ≤ᵇ n | ≤ᵇ→≤ m n | ≤→≤ᵇ {m} {n}
...        | true   | p        | _  = yes (p tt)
...        | false  | _        | ¬p = no ¬p

⌊_⌋ : ∀ {a : Set} → Dec a → Bool
⌊ yes x ⌋ = true
⌊ no ¬x ⌋ = false

_≤ᵇ'_ : ℕ → ℕ → Bool
m ≤ᵇ' n = ⌊ m ≤? n ⌋

toWitness : ∀ {a : Set} {d : Dec a} → T ⌊ d ⌋ → a
toWitness {a} {yes x} tt = x

fromWitness : ∀ {a : Set} {d : Dec a} → a → T ⌊ d ⌋
fromWitness {a} {yes x} _ = tt
fromWitness {a} {no ¬x} x = ¬x x

≤ᵇ'→≤ : ∀ {m n : ℕ} → T (m ≤ᵇ' n) → m ≤ n
≤ᵇ'→≤ = toWitness

≤→≤ᵇ' : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ' n)
≤→≤ᵇ' = fromWitness

infixr 6 _∧_

_∧_ : Bool → Bool → Bool
true ∧ true = true
_    ∧ _    = false

infixr 6 _×-dec_

_×-dec_ : ∀ {a b : Set} → Dec a → Dec b → Dec (a × b)
yes x ×-dec yes y = yes (x , y)
no ¬x ×-dec _     = no λ { (x , y) → ¬x x }
_     ×-dec no ¬y = no λ { (x , y) → ¬y y }

infixr 5 _∨_

_∨_ : Bool → Bool → Bool
false ∨ false = false
_     ∨ _     = true

infixr 5 _⊎-dec_

_⊎-dec_ : ∀ {a b : Set} → Dec a → Dec b → Dec (a ⊎ b)
yes x ⊎-dec _     = yes (inj₁ x)
_     ⊎-dec yes y = yes (inj₂ y)
no ¬x ⊎-dec no ¬y = no λ { (inj₁ x) → ¬x x ; (inj₂ y) → ¬y y }

not : Bool → Bool
not true  = false
not false = true

¬? : ∀ {a : Set} → Dec a → Dec (¬ a)
¬? (yes x) = no λ ¬x → ¬x x
¬? (no ¬x) = yes λ x → ¬x x

_⊃_ : Bool → Bool → Bool
true ⊃ false = false
_    ⊃ _     = true

_→-dec_ : ∀ {a b : Set} → Dec a → Dec b → Dec (a → b)
yes a →-dec no ¬b = no λ a→b → ¬b (a→b a)
_     →-dec yes b = yes λ a → b
no ¬a →-dec _     = yes λ a → ⊥-elim (¬a a)

∧-× : ∀ {a b : Set} (x : Dec a) (y : Dec b) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
∧-× (yes x) (yes y) = refl
∧-× (no ¬x) _       = refl
∧-× (yes x) (no ¬x) = refl

∨-⊎ : ∀ {a b : Set} (x : Dec a) (y : Dec b) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
∨-⊎ (no ¬x) (no ¬y) = refl
∨-⊎ (yes x) _       = refl
∨-⊎ (no ¬x) (yes x) = refl

not-¬ : ∀ {a : Set} (x : Dec a) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
not-¬ (yes x) = refl
not-¬ (no ¬x) = refl

-- https://gist.github.com/pedrominicz/bce9bcfc44f55c04ee5e0b6d903f5809
open import Isomorphism using (_⇔_)
open _⇔_

_iff_ : Bool → Bool → Bool
true  iff true  = true
false iff false = true
_     iff _     = false

_⇔-dec_ : ∀ {a b : Set} → Dec a → Dec b → Dec (a ⇔ b)
yes a ⇔-dec yes b = yes record { to = λ a → b ; from = λ b → a }
yes a ⇔-dec no ¬b = no λ a⇔b → ¬b (to a⇔b a)
no ¬a ⇔-dec yes b = no λ a⇔b → ¬a (from a⇔b b)
no ¬a ⇔-dec no ¬b = yes record { to = λ a → ⊥-elim (¬a a) ; from = λ b → ⊥-elim (¬b b) }

iff-⇔ : ∀ {a b : Set} (x : Dec a) (y : Dec b) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
iff-⇔ (yes x) (yes y) = refl
iff-⇔ (yes x) (no ¬y) = refl
iff-⇔ (no ¬x) (yes y) = refl
iff-⇔ (no ¬x) (no ¬y) = refl