Double negation embedding

Classical.agda

module Classical where

open import Function using (_∘_; case_of_; id; _$_)
open import Data.Product using (_×_; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Bool
  using (Bool; true; false; not; if_then_else_)
  renaming (_∨_ to _b∨_; _∧_ to _b∧_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; cong₂; sym; trans)
open import Relation.Nullary using (¬_)

infixr 6 !_
infixr 5 _∨_ _∧_
infixr 4 _⇒_ _⇔_

data PropTerm (A : Set) : Set where
  var : A → PropTerm A
  true false : PropTerm A
  !_ : PropTerm A → PropTerm A
  _∨_ _∧_ _⇒_ _⇔_ : (t u : PropTerm A) → PropTerm A

interpret : ∀ {A} → (A → Bool) → PropTerm A → Bool
interpret f (var x) = f x
interpret f true = true
interpret f false = false
interpret f (! t) = not (interpret f t)
interpret f (t ∨ u) = interpret f t b∨ interpret f u
interpret f (t ∧ u) = interpret f t b∧ interpret f u
interpret f (t ⇒ u) = not (interpret f t) b∨ interpret f u
interpret f (t ⇔ u) =
  if interpret f t then interpret f u else not (interpret f u)

infix 4 _↔_
_↔_ : (A B : Set) → Set
A ↔ B = (A → B) × (B → A)

Prop→Set : ∀ {A} → (A → Set) → PropTerm A → Set
Prop→Set f (var x) = f x
Prop→Set f true = ⊤
Prop→Set f false = ⊥
Prop→Set f (! t) = ¬ Prop→Set f t
Prop→Set f (t ∨ u) = Prop→Set f t ⊎ Prop→Set f u
Prop→Set f (t ∧ u) = Prop→Set f t × Prop→Set f u
Prop→Set f (t ⇒ u) = Prop→Set f t → Prop→Set f u
Prop→Set f (t ⇔ u) = Prop→Set f t ↔ Prop→Set f u

infixr 6 s!_
infixr 5 _s∧_

data SimpleTerm (A : Set) : Set where
  svar : A → SimpleTerm A
  strue sfalse : SimpleTerm A
  s!_ : SimpleTerm A → SimpleTerm A
  _s∧_ : (t u : SimpleTerm A) → SimpleTerm A

sinterpret : ∀ {A} → (A → Bool) → SimpleTerm A → Bool
sinterpret f (svar x) = f x
sinterpret f strue = true
sinterpret f sfalse = false
sinterpret f (s! t) = not (sinterpret f t)
sinterpret f (t s∧ u) = sinterpret f t b∧ sinterpret f u

Simple→Set : ∀ {A} → (A → Set) → SimpleTerm A → Set
Simple→Set f (svar x) = f x
Simple→Set f strue = ⊤
Simple→Set f sfalse = ⊥
Simple→Set f (s! t) = ¬ Simple→Set f t
Simple→Set f (t s∧ u) = Simple→Set f t × Simple→Set f u

simplify : ∀ {A} → PropTerm A → SimpleTerm A
simplify (var x) = svar x
simplify true = strue
simplify false = sfalse
simplify (! t) = s! simplify t
simplify (t ∨ u) = s! (s! simplify t s∧ s! simplify u)
simplify (t ∧ u) = simplify t s∧ simplify u
simplify (t ⇒ u) = s! (simplify t s∧ s! simplify u)
simplify (t ⇔ u) =
  let st = simplify t in
  let su = simplify u in
  s! (st s∧ s! su) s∧ s! (su s∧ s! st)

∨≡¬[¬∧¬] : ∀ x y → x b∨ y ≡ not (not x b∧ not y)
∨≡¬[¬∧¬] false false = refl
∨≡¬[¬∧¬] false true = refl
∨≡¬[¬∧¬] true _ = refl

¬∨≡¬[∧¬] : ∀ x y → not x b∨ y ≡ not (x b∧ not y)
¬∨≡¬[∧¬] false y = refl
¬∨≡¬[∧¬] true false = refl
¬∨≡¬[∧¬] true true = refl

⇔-simplify :
  ∀ x y → (if x then y else not y) ≡ not (x b∧ not y) b∧ not (y b∧ not x)
⇔-simplify false false = refl
⇔-simplify false true = refl
⇔-simplify true false = refl
⇔-simplify true true = refl

simplify-correct :
  ∀ {A} (f : A → Bool) (t : PropTerm A) →
  interpret f t ≡ sinterpret f (simplify t)
simplify-correct f (var x) = refl
simplify-correct f true = refl
simplify-correct f false = refl
simplify-correct f (! t) = cong not (simplify-correct f t)
simplify-correct f (t ∨ u) =
  trans (cong₂ _b∨_ (simplify-correct f t) (simplify-correct f u))
        (∨≡¬[¬∧¬] (sinterpret f (simplify t)) (sinterpret f (simplify u)))
simplify-correct f (t ∧ u) =
  cong₂ (_b∧_) (simplify-correct f t) (simplify-correct f u)
simplify-correct f (t ⇒ u) =
  trans
    (cong₂ (λ x y → not x b∨ y) (simplify-correct f t) (simplify-correct f u))
    (¬∨≡¬[∧¬] (sinterpret f (simplify t)) (sinterpret f (simplify u)))
simplify-correct f (t ⇔ u) =
  trans (cong₂ (λ x y → if x then y else not y) (simplify-correct f t)
                                                (simplify-correct f u))
        (⇔-simplify (sinterpret f (simplify t)) (sinterpret f (simplify u)))

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

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

LEM : ∀ {a} (A : Set a) → ¬ ¬ (A ⊎ ¬ A)
LEM _ p =
  let ¬A = p ∘ inj₁ in
  let ¬¬A = p ∘ inj₂ in
  ¬¬A ¬A

pure : ∀ {a} {A : Set a} → A → ¬ ¬ A
pure A = λ z → z A

infixl 1 _>>=_
_>>=_ : ∀ {a b} {A : Set a} {B : Set b} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B
_>>=_ ¬¬A A→¬¬B ¬B = ¬¬A ((λ ¬¬B → ¬¬B ¬B) ∘  A→¬¬B)

¬[¬×¬]→¬¬⊎ : ∀ {a b} {A : Set a} {B : Set b} → ¬ (¬ A × ¬ B) → ¬ ¬ (A ⊎ B)
¬[¬×¬]→¬¬⊎ {A = A} {B} p =
  LEM A >>= λ A⊎¬A →
  case A⊎¬A of λ
  { (inj₁ A) → pure (inj₁ A)
  ; (inj₂ ¬A) →
    LEM B >>= λ B⊎¬B →
    case B⊎¬B of λ
    { (inj₁ B) → pure (inj₂ B)
    ; (inj₂ ¬B) → ⊥-elim (p (¬A , ¬B))
    }
  }

contranegative-lemma :
  ∀ {a b} {A : Set a} {B : Set b} →
  ((B → ⊥) → (A → ⊥)) → (A → ¬ ¬ B)
contranegative-lemma f a ¬b = f ¬b a

¬¬-pull :
  ∀ {a b} {A : Set a} {B : Set b} →
  (A → ¬ ¬ B) → ¬ ¬ (A → B)
¬¬-pull {A = A} f =
  LEM A >>= λ a⊎¬a →
  case a⊎¬a of λ
  { (inj₁ a) → f a >>= λ b → pure (λ _ → b)
  ; (inj₂ ¬a) → pure (λ a → ⊥-elim (¬a a))
  }

contranegative :
  ∀ {a b} {A : Set a} {B : Set b} →
  ((B → ⊥) → (A → ⊥)) → ¬ ¬ (A → B)
contranegative {A = A} {B} f = ¬¬-pull (contranegative-lemma f)

⊥-prop : ¬ ¬ ⊥ → ⊥
⊥-prop f = f id

SimpleSet→¬¬PropSet :
  ∀ {A} (f : A → Bool) (t : PropTerm A) →
  Simple→Set (_≡_ true ∘ f) (simplify t) → ¬ ¬ Prop→Set (_≡_ true ∘ f) t
PropSet→SimpleSet :
  ∀ {A} (f : A → Bool) (t : PropTerm A) →
  Prop→Set (_≡_ true ∘ f) t → Simple→Set (_≡_ true ∘ f) (simplify t)

SimpleSet→¬¬PropSet f (var x) p = pure p
SimpleSet→¬¬PropSet f true p = pure p
SimpleSet→¬¬PropSet f false p = pure p
SimpleSet→¬¬PropSet f (! t) p = pure (λ q → p (PropSet→SimpleSet f t q))
SimpleSet→¬¬PropSet f (t ∨ u) p =
  ¬[¬×¬]→¬¬⊎ p >>= λ s →
  case s of λ
  { (inj₁ ts) → SimpleSet→¬¬PropSet f t ts >>= λ tp → pure (inj₁ tp)
  ; (inj₂ us) → SimpleSet→¬¬PropSet f u us >>= λ up → pure (inj₂ up)
  }
SimpleSet→¬¬PropSet f (t ∧ u) (tp , up) =
  SimpleSet→¬¬PropSet f t tp >>= λ ts →
  SimpleSet→¬¬PropSet f u up >>= λ us →
  pure (ts , us)
SimpleSet→¬¬PropSet f (t ⇒ u) p =
  contranegative (λ ¬up tp →
    p (PropSet→SimpleSet f t tp , (λ us → SimpleSet→¬¬PropSet f u us ¬up)))
SimpleSet→¬¬PropSet f (t ⇔ u) (pr , pl) =
  ¬¬-pull (λ ts ¬us → pr (ts , ¬us)) >>= λ pr′ →
  ¬¬-pull (λ us ¬ts → pl (us , ¬ts)) >>= λ pl′ →
  ¬¬-pull (SimpleSet→¬¬PropSet f u ∘ pr′ ∘ PropSet→SimpleSet f t) >>= λ pr″ →
  ¬¬-pull (SimpleSet→¬¬PropSet f t ∘ pl′ ∘ PropSet→SimpleSet f u) >>= λ pl″ →
  pure (pr″ , pl″)

PropSet→SimpleSet f (var x) p = p
PropSet→SimpleSet f true p = p
PropSet→SimpleSet f false p = p
PropSet→SimpleSet f (! t) p s = SimpleSet→¬¬PropSet f t s p
PropSet→SimpleSet f (t ∨ u) (inj₁ tp) (¬ts , _) =
  ¬ts (PropSet→SimpleSet f t tp)
PropSet→SimpleSet f (t ∨ u) (inj₂ up) (_ , ¬us) =
  ¬us (PropSet→SimpleSet f u up)
PropSet→SimpleSet f (t ∧ u) (tp , up) =
  PropSet→SimpleSet f t tp , PropSet→SimpleSet f u up
PropSet→SimpleSet f (t ⇒ u) p (ts , ¬us) = ⊥-prop $
  SimpleSet→¬¬PropSet f t ts >>= λ tp →
  pure $ ¬us (PropSet→SimpleSet f u (p tp))
PropSet→SimpleSet f (t ⇔ u) (pr , pl) =
  (λ { (ts , ¬us) → ⊥-prop $
    SimpleSet→¬¬PropSet f t ts >>= λ tp →
    pure $ ¬us (PropSet→SimpleSet f u (pr tp)) })
  ,
  (λ { (us , ¬ts) → ⊥-prop $
    SimpleSet→¬¬PropSet f u us >>= λ up →
    pure $ ¬ts (PropSet→SimpleSet f t (pl up)) })

not-not : ∀ x → not (not x) ≡ x
not-not false = refl
not-not true = refl

∧-sym : ∀ x y → x b∧ y ≡ y b∧ x
∧-sym false false = refl
∧-sym false true = refl
∧-sym true false = refl
∧-sym true true = refl

true-proj₁ : ∀ {x y} → true ≡ x b∧ y → true ≡ x
true-proj₁ {false} ()
true-proj₁ {true} p = refl

true-proj₂ : ∀ {x y} → true ≡ x b∧ y → true ≡ y
true-proj₂ {false} {false} ()
true-proj₂ {true} {false} ()
true-proj₂ {_} {true} p = refl

true-case :
  ∀ {x y p} (P : Bool → Set p) →
  true ≡ x b∨ y → (true ≡ x → P false) → (true ≡ y → P true) → P false ⊎ P true
true-case {false} {false} _ () f g
true-case {false} {true} _ p f g = inj₂ (g p)
true-case {true} {_} _ p f g = inj₁ (f p)

⇔-true : ∀ {x y} → true ≡ (if x then y else not y) → x ≡ y
⇔-true {false} {false} p = refl
⇔-true {false} {true} ()
⇔-true {true} {false} ()
⇔-true {true} {true} p = refl

false-proj₁ : ∀ {x y} → false ≡ x b∨ y → false ≡ x
false-proj₁ {false} p = refl
false-proj₁ {true} ()

false-proj₂ : ∀ {x y} → false ≡ x b∨ y → false ≡ y
false-proj₂ {_} {false} p = refl
false-proj₂ {false} {true} ()
false-proj₂ {true} {true} ()

false-case :
  ∀ {x y p} (P : Bool → Set p) →
  false ≡ x b∧ y → (false ≡ x → P false) → (false ≡ y → P true) → P false ⊎ P true
false-case {false} {_} _ p f g = inj₁ (f p)
false-case {true} {false} _ p f g = inj₂ (g p)
false-case {true} {true} _ () f g

sembed :
  ∀ {A} (f : A → Bool) (t : SimpleTerm A) →
  true ≡ sinterpret f t → ¬ ¬ Simple→Set (_≡_ true ∘ f) t
¬sembed :
  ∀ {A} (f : A → Bool) (t : SimpleTerm A) →
  false ≡ sinterpret f t → ¬ Simple→Set (_≡_ true ∘ f) t

sembed f (svar x) p = pure p
sembed f strue p = pure tt
sembed f sfalse ()
sembed f (s! t) p = pure (¬sembed f t (trans (cong not p) (not-not _)))
sembed f (t s∧ u) p =
  sembed f t (true-proj₁ p) >>= λ ts →
  sembed f u (true-proj₂ {sinterpret f t} p) >>= λ us →
  pure (ts , us)

¬sembed f (svar x) p z with trans p (sym z)
¬sembed f (svar x) p z | ()
¬sembed f strue ()
¬sembed f sfalse p z = z
¬sembed f (s! t) p = sembed f t (trans (cong not p) (not-not _))
¬sembed f (t s∧ u) p (x , y) =
  case (false-case P p (¬sembed f t) (¬sembed f u)) of λ
  { (inj₁ ¬ts) → ¬ts x
  ; (inj₂ ¬us) → ¬us y
  }
  where
    P : Bool → Set
    P false = ¬ Simple→Set (_≡_ true ∘ f) t
    P true = ¬ Simple→Set (_≡_ true ∘ f) u

embed :
  ∀ {A} (f : A → Bool) (t : PropTerm A) →
  true ≡ interpret f t → ¬ ¬ Prop→Set (_≡_ true ∘ f) t
embed f t p =
  sembed f (simplify t) (trans p (simplify-correct f t)) >>= λ ss →
  SimpleSet→¬¬PropSet f t ss