Programming Language Foundations in Agda: Negation

Negation.agda

module Negation where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)
open import Data.Nat.Properties using (+-identityʳ)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂; swap)
open import Function using (_∘_)

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

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

¬_ : Set → Set
¬ A = A → ⊥

infixr 20 ¬_

¬¬-intro : ∀ {A : Set} → A → ¬ ¬ A
¬¬-intro a = λ { ¬a → ¬a a }

¬¬¬-elim : ∀ {A : Set} → ¬ ¬ ¬ A → ¬ A
¬¬¬-elim ¬¬¬a = λ a → ¬¬¬a (¬¬-intro a)

contraposition : ∀ {A B : Set} → (A → B) → ¬ B → ¬ A
contraposition f ¬b = λ { a → ¬b (f a) }

_≢_ : ∀ {A : Set} → A → A → Set
x ≢ y = ¬ ( x ≡ y )

peano : ∀ {n : ℕ} → zero ≢ suc n
peano = λ ()

<-irreflexive : ∀ {n : ℕ} → ¬ (n < n)
<-irreflexive {zero}  = λ ()
<-irreflexive {suc n} = λ { (s<s n<n) → <-irreflexive {n} n<n }

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

trichotomy : ∀ {n m : ℕ}
    → (n < m × ¬(n ≡ m) × ¬(m < n))
    ⊎ (¬(n < m) × n ≡ m × ¬(m < n))
    ⊎ (¬(n < m) × ¬(n ≡ m) × m < n)
trichotomy {zero}  {zero}  = inj₂ (inj₁ ((λ ()) , refl , λ ()))
trichotomy {zero}  {suc m} = inj₁ (z<s , (λ ()) , λ ())
trichotomy {suc n} {zero}  = inj₂ (inj₂ ((λ ()) , (λ ()) , z<s))
trichotomy {suc n} {suc m} with trichotomy {n} {m}
...                           | inj₂ (inj₁ (f , x , g)) = inj₂ (inj₁ ((λ { (s<s n<m) → f n<m } ) , cong suc x , (λ { (s<s m<n) → g m<n } )))
...                           | inj₁ (x , f , g)        = inj₁ (s<s x , (λ n≡m → f (pred n≡m)) , (λ { (s<s m<n) → g m<n } ))
...                           | inj₂ (inj₂ (f , g , x)) = inj₂ (inj₂ ((λ { (s<s n<m) → f n<m } ) , (λ n≡m → g (pred n≡m)) , s<s x))

⊎-dual-× : ∀ {A B : Set} → ¬(A ⊎ B) ≃ ¬ A × ¬ B
⊎-dual-× {A} {B} =
    record
        { to      = to
        ; from    = from
        ; from∘to = λ { f → extensionality λ { (inj₁ x) → refl ; (inj₂ x) → refl } }
        ; to∘from = λ { f → refl }
        }
    where
    to : ¬(A ⊎ B) → ¬ A × ¬ B
    to f = (λ x → f (inj₁ x)) , (λ x → f (inj₂ x))

    from : ¬ A × ¬ B → ¬(A ⊎ B)
    from (f , g) = λ { (inj₁ x) → f x ; (inj₂ x) → g x }

module Excluded-Middle where
    postulate
        em : ∀ {A : Set} → A ⊎ ¬ A

    em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
    em-irrefutable = λ ¬em → ¬em (inj₂ (λ a → ¬em (inj₁ a)))

    ¬¬-elim : ∀ {A : Set} → ¬ ¬ A → A
    ¬¬-elim {A} ¬¬a = em-elim em
        where
        em-elim : A ⊎ ¬ A → A
        em-elim (inj₁ a)  = a
        em-elim (inj₂ ¬a) = ⊥-elim (¬¬a ¬a)

    peirce-law : ∀ {A B : Set} → ((A → B) → A) → A
    peirce-law {A} {B} ⟨a→b⟩→a = em-elim em
        where
        em-elim : A ⊎ ¬ A → A
        em-elim (inj₁ a)  = a
        em-elim (inj₂ ¬a) = ⟨a→b⟩→a (λ a → ⊥-elim (¬a a))

    impl-disj : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
    impl-disj {A} {B} a→b = em-elim em
        where
        em-elim : A ⊎ ¬ A → ¬ A ⊎ B
        em-elim (inj₁ a)  = inj₂ (a→b a)
        em-elim (inj₂ ¬a) = inj₁ ¬a

    de-morgan : ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B
    de-morgan {A} {B} ¬⟨¬a׬b⟩ = em-elim em
        where
        helper : B ⊎ ¬ B → ¬ A → B
        helper (inj₁ b)  ¬a = b
        helper (inj₂ ¬b) ¬a = ⊥-elim (¬⟨¬a׬b⟩ (¬a , ¬b))

        em-elim : A ⊎ ¬ A → A ⊎ B
        em-elim (inj₁ a)  = inj₁ a
        em-elim (inj₂ ¬a) = inj₂ (helper em ¬a)

module Double-Negation where
    postulate
        ¬¬-elim : ∀ {A : Set} → ¬ ¬ A → A

    excluded-middle : ∀ {A : Set} → A ⊎ ¬ A
    excluded-middle {A} = ¬¬-elim λ ¬r → ¬r (inj₂ λ a → ¬r (inj₁ a))

    peirce-law : ∀ {A B : Set} → ((A → B) → A) → A
    peirce-law {A} {B} ⟨a→b⟩→a = ¬¬-elim λ ¬a → ¬a (⟨a→b⟩→a (helper ¬a))
        where
        helper : ¬ A → A → B
        helper ¬a a = ⊥-elim (¬a a)

    impl-disj : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
    impl-disj {A} {B} a→b = ¬¬-elim λ ¬r → ¬r (inj₁ λ a → ¬r (inj₂ (a→b a)))

    de-morgan : ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B
    de-morgan {A} {B} ¬⟨¬a׬b⟩ = ¬¬-elim λ ¬r → ¬⟨¬a׬b⟩ (helper ¬r)
        where
        ¬r→¬a : ¬ (A ⊎ B) → ¬ A
        ¬r→¬a ¬r a = ¬r (inj₁ a)

        ¬r→¬b : ¬ (A ⊎ B) → ¬ B
        ¬r→¬b ¬r b = ¬r (inj₂ b)

        helper : ¬ (A ⊎ B) → ¬ A × ¬ B
        helper ¬r = (¬r→¬a ¬r , ¬r→¬b ¬r)

module Pierce-Law where
    peirce-law-irrefutable : ∀ {A B : Set} → ¬ ¬ (((A → B) → A) → A)
    peirce-law-irrefutable {A} {B} ¬peirce-law = ¬peirce-law peirce-law
        where
        const : A → ((A → B) → A) → A
        const a ⟨a→b⟩→a = a

        a→b : A → B
        a→b a = ⊥-elim (¬peirce-law (const a))

        peirce-law : ((A → B) → A) → A
        peirce-law ⟨a→b⟩→a = ⟨a→b⟩→a a→b

    postulate
        peirce-law : ∀ {A B : Set} → ((A → B) → A) → A

    excluded-middle : ∀ {A : Set} → A ⊎ ¬ A
    excluded-middle {A} = peirce-law λ ¬r → inj₂ λ a → ¬r (inj₁ a)

    ¬¬-elim : ∀ {A : Set} → ¬ ¬ A → A
    ¬¬-elim {A} ¬¬a = peirce-law λ ¬a → ⊥-elim (¬¬a λ a → ¬a a)

    impl-disj : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
    impl-disj {A} {B} a→b = peirce-law λ ¬r → inj₁ λ a → ¬r (inj₂ (a→b a))

    de-morgan : ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B
    de-morgan {A} {B} ¬⟨¬a׬b⟩ = peirce-law λ ¬r → ⊥-elim (¬⟨¬a׬b⟩ (helper₁ ¬r , helper₂ ¬r))
        where
        helper₁ : ¬ (A ⊎ B) → ¬ A
        helper₁ ¬r a = ¬r (inj₁ a)

        helper₂ : ¬ (A ⊎ B) → ¬ B
        helper₂ ¬r b = ¬r (inj₂ b)

module Implication-as-Disjunction where
    postulate
        impl-disj : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B

    excluded-middle : ∀ {A : Set} → A ⊎ ¬ A
    excluded-middle {A} = swap (impl-disj (λ a → a))

    ¬¬-elim : ∀ {A : Set} → ¬ ¬ A → A
    ¬¬-elim {A} ¬¬a = em-elim (impl-disj (λ a → a))
        where
        em-elim : ¬ A ⊎ A → A
        em-elim (inj₁ ¬a) = ⊥-elim (¬¬a ¬a)
        em-elim (inj₂ a)  = a

    peirce-law : ∀ {A B : Set} → ((A → B) → A) → A
    peirce-law {A} {B} ⟨a→b⟩→a = em-elim (impl-disj (λ a → a))
        where
        em-elim : ¬ A ⊎ A → A
        em-elim (inj₁ ¬a) = ⟨a→b⟩→a (λ a → ⊥-elim (¬a a))
        em-elim (inj₂ a)  = a

    de-morgan : ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B
    de-morgan {A} {B} ¬⟨¬a׬b⟩ = go (impl-disj (λ a → a) , impl-disj (λ b → b))
        where
        go : (¬ A ⊎ A) × (¬ B ⊎ B) → A ⊎ B
        go (inj₁ ¬a , inj₁ ¬b) = ⊥-elim (¬⟨¬a׬b⟩ (¬a , ¬b))
        go (inj₂ a  , _      ) = inj₁ a
        go (_       , inj₂ b ) = inj₂ b

module De-Morgan where
    postulate
        de-morgan : ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B

    excluded-middle : ∀ {A : Set} → A ⊎ ¬ A
    excluded-middle {A} = de-morgan λ { (¬a , ¬¬a) → ¬¬a ¬a }

    ¬¬-elim : ∀ {A : Set} → ¬ ¬ A → A
    ¬¬-elim {A} ¬¬a = helper (de-morgan λ { (¬a , ¬a') → ¬¬a ¬a })
        where
        helper : A ⊎ A → A
        helper (inj₁ a) = a
        helper (inj₂ a) = a

    peirce-law : ∀ {A B : Set} → ((A → B) → A) → A
    peirce-law {A} {B} ⟨a→b⟩→a = helper₁ (de-morgan helper₂)
        where
        const : B → A → B
        const b a = b

        helper₁ : A ⊎ B → A
        helper₁ (inj₁ a) = a
        helper₁ (inj₂ b) = ⟨a→b⟩→a (const b)

        helper₂ : ¬ (¬ A × ¬ B)
        helper₂ (¬a , ¬b) = ¬a (⟨a→b⟩→a λ a → ⊥-elim (¬a a))

    impl-disj : ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
    impl-disj {A} {B} a→b = de-morgan λ { (¬¬a , ¬b) → ¬b (a→b (¬¬-elim ¬¬a)) }

Stable : Set → Set
Stable A = ¬ ¬ A → A

¬-stable : ∀ {A : Set} → Stable (¬ A)
¬-stable = λ ¬¬¬a → ¬¬¬-elim ¬¬¬a

×-stable : ∀ {A B : Set} → Stable A → Stable B → Stable (A × B)
×-stable {A} {B} ¬¬a→a ¬¬b→b ¬¬⟨a×b⟩ = go helper₁ helper₂
    where
    helper₁ : ¬ ¬ A
    helper₁ = λ ¬a → ¬¬⟨a×b⟩ (λ a×b → ¬a (proj₁ a×b))

    helper₂ : ¬ ¬ B
    helper₂ = λ ¬b → ¬¬⟨a×b⟩ (λ a×b → ¬b (proj₂ a×b))

    go : ¬ ¬ A → ¬ ¬ B → A × B
    go ¬¬a ¬¬b = (¬¬a→a ¬¬a , ¬¬b→b ¬¬b)