Flip.agda

module Flip where

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- truth values

data Truth : Set where
  ⊤ : Truth
  ⊥ : Truth

infixr 5 _or_
infixr 6 _and_
infix  7 not_

_or_ : Truth → Truth → Truth
⊥ or ⊥ = ⊥
⊥ or ⊤ = ⊤
⊤ or ⊥ = ⊤
⊤ or ⊤ = ⊤

_and_ : Truth → Truth → Truth
⊤ and ⊤ = ⊤
⊤ and ⊥ = ⊥
⊥ and ⊤ = ⊥
⊥ and ⊥ = ⊥

not_ : Truth → Truth
not ⊤ = ⊥
not ⊥ = ⊤

-- basic equivalences of truth values

double-negation : ∀ {x} → x ≡ not not x
double-negation {⊤} = refl
double-negation {⊥} = refl

demorgan-or : ∀ {x y} → not x or not y ≡ not (x and y)
demorgan-or {⊤} {⊤} = refl
demorgan-or {⊤} {⊥} = refl
demorgan-or {⊥} {⊤} = refl
demorgan-or {⊥} {⊥} = refl

demorgan-and : ∀ {x y} → not x and not y ≡ not (x or y)
demorgan-and {⊤} {⊤} = refl
demorgan-and {⊤} {⊥} = refl
demorgan-and {⊥} {⊤} = refl
demorgan-and {⊥} {⊥} = refl

-- logic formula with only conjunction, disjunction and negation

infixr 1 _of_

_of_ : ∀ {ℓ} {A B : Set ℓ} → (A → B) → A → B
f of x = f x

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

data Formula (V : Set) : Set where
  var   : V → Formula of V
  const : Truth → Formula of V
  _∨_   : Formula of V → Formula of V → Formula of V
  _∧_   : Formula of V → Formula of V → Formula of V
  ¬_    : Formula of V → Formula of V

-- assignment of truth values to formulae

Assignment : Set → Set
Assignment V = V → Truth

negate : ∀ {V} → Assignment of V → Assignment of V
negate σ x = not (σ x)

infix 7 _[_]

_[_] : ∀ {V} → Formula of V → Assignment of V → Truth
(var x)   [ σ ] = σ x
(const t) [ _ ] = t
(A ∧ B)   [ σ ] = A [ σ ] and B [ σ ]
(A ∨ B)   [ σ ] = A [ σ ] or  B [ σ ]
(¬ A)     [ σ ] = not (A [ σ ])

-- what we mean by a tautology and a contradiction

infixl 0 _is_

_is_ : ∀ {ℓ ℓ′} {A : Set ℓ} → A → (A → Set ℓ′) → Set ℓ′
x is P = P x

tautology : ∀ {V} → Formula of V → Set
tautology {V} A = ∀ (σ : Assignment V) → A [ σ ] ≡ ⊤

contradiction : ∀ {V} → Formula of V → Set
contradiction {V} A = ∀ (σ : Assignment V) → A [ σ ] ≡ ⊥

-- the titular 'flip' operation

flip : ∀ {V} → Formula of V → Formula of V
flip (var x)   = var x
flip (const t) = const (not t)
flip (A ∧ B)   = flip A ∨ flip B
flip (A ∨ B)   = flip A ∧ flip B
flip (¬ A)     = ¬ flip A

-- Dennis' proof

lem₁ : ∀ {V} (σ : Assignment of V) (A : Formula of V) → (flip A) [ σ ] ≡ not (A [ negate σ ])
lem₁ σ (var x)                             = double-negation
lem₁ σ (const t)                           = refl
lem₁ σ (A ∧ B) rewrite lem₁ σ A | lem₁ σ B = demorgan-or
lem₁ σ (A ∨ B) rewrite lem₁ σ A | lem₁ σ B = demorgan-and
lem₁ σ (¬ A)   rewrite lem₁ σ A            = refl

theorem : ∀ {V} (A : Formula of V) → A is tautology → flip A is contradiction
theorem A A⊤ σ rewrite lem₁ σ A | A⊤ (negate σ) = refl