Skip to content

Instantly share code, notes, and snippets.

@domandlj

domandlj/Lem.agda

Created June 19, 2023 16:51
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save domandlj/760725d8aaa06e08fb7ea0e75a37ac54 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save domandlj/760725d8aaa06e08fb7ea0e75a37ac54 to your computer and use it in GitHub Desktop.
Download ZIP
Law of excluded middle and decision procedures.
Raw
Lem.agda
module LEM where
open import Data.Nat
open import Data.Bool
open import Relation.Nullary using (¬_)
open import Data.Sum using (inj₁; inj₂) renaming (_⊎_ to _∨_)
open import Relation.Nullary using (Dec; yes; no)
-- A predicate about if nat is even.
data Even : ℕ → Set where
even-zero : Even 0
even-suc : ∀ n
→ Even n
----------------
→ Even (suc (suc n))
postulate
-- The law of excluded middle.
lem : ∀ {P : Set} → P ∨ ¬ P
-- Can we decide if natural is even?
-- Proof using LEM
even-dec₁ : ∀ n → Even n ∨ ¬ Even n
even-dec₁ n = lem
-- We prove this but we don't get anything to compute out of it :(.
-- We can give a decision procedure for the predicate Even.
even? : ∀ n → Dec (Even n)
even? zero = yes even-zero
even? (suc zero) = no (λ ())
even? (suc (suc n)) with even? n
... | yes even-n = yes (even-suc n even-n)
... | no ¬even-n = no (lemma n ¬even-n)
where
lemma : ∀ n → ¬ Even n → ¬ Even (suc (suc n))
lemma n ¬even-n (even-suc .n p) = ¬even-n p
-- Try to normalize this.
is-even : ℕ → Bool
is-even n with even? n
... | yes _ = true
... | no _ = false
-- Proof not using LEM
even-dec₂ : ∀ n → Even n ∨ ¬ Even n
even-dec₂ n with even? n
... | yes even-n = inj₁ even-n
... | no ¬even-n = inj₂ ¬even-n
-- So, if we prove this that means we must have a decision procedure to decide it.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment