Duality of propositional logic.

Dual.agda

module Dual where

open import Agda.Builtin.Equality

data Bool : Set where
    ⊤ : Bool
    ⊥ : Bool

not : Bool → Bool
not ⊤ = ⊥
not ⊥ = ⊤

_&&_ : Bool → Bool → Bool
⊤ && ⊤ = ⊤
_ && _ = ⊥

_||_ : Bool → Bool → Bool
⊥ || ⊥ = ⊥
_ || _ = ⊤

infixr 6 _&&_
infixr 5 _||_

data Term : Set where
    ¬_ : Term → Term
    _∧_ : Term → Term → Term
    _∨_ : Term → Term → Term
    ⊤ : Term
    ⊥ : Term

infix 7 ¬_
infixr 6 _∧_
infixr 5 _∨_

_⇒_ : Term → Term → Term
p ⇒ q = ¬ p ∨ q

eval : Term → Bool
eval (¬ p)   = not (eval p)
eval (p ∧ q) = eval p && eval q
eval (p ∨ q) = eval p || eval q
eval ⊤       = ⊤
eval ⊥       = ⊥

dual : Term → Term
dual (¬ p)   = p
dual (p ∧ q) = dual p ∨ dual q
dual (p ∨ q) = dual p ∧ dual q
dual ⊤       = ⊥
dual ⊥       = ⊤

lemma-1 : ∀ p → not (not p) ≡ p
lemma-1 ⊤ = refl
lemma-1 ⊥ = refl

lemma-2 : ∀ p q → not p || not q ≡ not (p && q)
lemma-2 ⊤ ⊤ = refl
lemma-2 ⊤ ⊥ = refl
lemma-2 ⊥ ⊤ = refl
lemma-2 ⊥ ⊥ = refl

lemma-3 : ∀ p q → not p && not q ≡ not (p || q)
lemma-3 ⊤ ⊤ = refl
lemma-3 ⊤ ⊥ = refl
lemma-3 ⊥ ⊤ = refl
lemma-3 ⊥ ⊥ = refl

theorem : ∀ p → eval (dual p) ≡ not (eval p)
theorem (¬ p)
    rewrite theorem p | lemma-1 (eval p) = refl
theorem (p ∧ q)
    rewrite theorem p | theorem q | lemma-2 (eval p) (eval q) = refl
theorem (p ∨ q)
    rewrite theorem p | theorem q | lemma-3 (eval p) (eval q) = refl
theorem ⊤ = refl
theorem ⊥ = refl