Decidability

{-# OPTIONS --allow-unsolved-metas --without-K #-}

open import Level using (Level)
import Level as L
open import Data.Nat
open import Data.Unit
open import Data.List hiding ([_])
open import Data.List.Properties as List
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.Bool hiding (_∨_; _∧_)
open import Function.Definitions using (Injective)
open import Function.Base using (_∘_; flip)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation using (¬_)

module Decidable where
private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Set ℓ
    B : Set ℓ'

Entscheidbarkeit

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

In the standard library, Dec is a record consisting of a Bool together with the corresponding proof of A or ¬ A. The reason is the separation of the computed result from its proof (explanation in the stdlib).

_B≡?_ : ∀ (x y : Bool) → Dec (x ≡ y)
false B≡? false = yes refl
false B≡? true = no λ { () }
true B≡? false = no (λ ())
true B≡? true = yes refl

⊤? : Dec ⊤
⊤? = yes tt
⊥? : Dec ⊥
⊥? = no λ ()

_is-injective : (f : A → B) → Set _
_is-injective f = ∀ {x} {y} → f x ≡ f y → x ≡ y

suc-is-injective : suc is-injective
suc-is-injective {n} {m} refl = refl

_ℕ≡?_ : ∀ (n m : ℕ) → Dec (n ≡ m)
zero ℕ≡? zero = yes refl
zero ℕ≡? suc m = no λ ()
suc n ℕ≡? zero = no λ ()
suc n ℕ≡? suc m with (n ℕ≡? m)
... | yes n≡m = yes (cong suc n≡m)
... | no n≢m = no (n≢m ∘ suc-is-injective)
-- with-abstraction = notation for:
-- suc n ℕ≡? suc m = helper (n ℕ≡? m)
--   where
--   helper : Dec (n ≡ m) → Dec (suc n ≡ suc m)
--   helper (yes n≡m) = yes (cong suc n≡m)
--   helper (no n≢m) = no (n≢m ∘ suc-is-injective)


Dec-map : (A → B) → (B → A) → Dec A → Dec B
Dec-map A→B B→A (yes a) = yes (A→B a)
Dec-map A→B B→A (no ¬a) = no (¬a ∘ B→A)

Decidability of relations

Decidable₂ : {A : Set ℓ} → (A → A → Set ℓ') → Set _
Decidable₂ _R_ = ∀ x x' → Dec (x R x')

Beispiele

L≡? : Decidable₂ (_≡_ {_} {A}) → Decidable₂ (_≡_ {_} {List A}) 
L≡? dec-A [] [] = yes refl 
L≡? dec-A [] (_ ∷ _) = no λ () 
L≡? dec-A (x ∷ xs) [] = no λ () 
L≡? dec-A (x ∷ xs) (y ∷ ys) with (dec-A x y)
... | yes refl = Dec-map (cong (x ∷_)) ∷-injectiveʳ (L≡? dec-A xs ys)
... | no x≢y = no (λ {refl → x≢y refl})
    --                 ^--- pattern-lambda


_ : ∀ (l1 l2 : List ℕ) → Dec (l1 ≡ l2)
_ = L≡? _ℕ≡?_

Logik

Disjunktion in Agda

infixr 1 _∨_
data _∨_ (A : Set ℓ) (B : Set ℓ') : Set (ℓ L.⊔ ℓ') where
  ∨E₁ : A → A ∨ B
  ∨E₂ : B → A ∨ B

Negation ¬ B = B → ⊥. Is the law of excluded middle derivable in Agda?

LEM : Set → Set _
LEM A = A ∨ ¬ A

¬¬LEM : ∀ (A : Set) → ¬ ¬ (LEM A)
¬¬LEM A ¬LEM = (¬LEM ∘ ∨E₂) (¬LEM ∘ ∨E₁)

contraposition : (A → B) → (¬ B → ¬ A)
contraposition f =  _∘ f

-- what about the other direction?
End of lecture on 30 April 2026

Stdlib

import Relation.Binary.PropositionalEquality using (_≗_) -- pointwise equality
import Relation.Binary using (Decidable) -- Decidable₂
import Relation.Nullary.Decidable using (Dec; map′)
import Function.Base using (case_of_)
import Function.Bundles using (Injection; _↣_; mk↣)
import Relation.Nullary.Negation using (contraposition)
import Data.Sum using (_⊎_) -- disjunction

Further references:

Agda Quellcode herunterladen