Double negation embedding

Classical.agda

module Classical where

open import Function using (_∘_; case_of_; id; _$_; _∋_)
open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂)
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_; T)
  renaming (_∨_ to _b∨_; _∧_ to _b∧_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; cong₂; sym; trans; subst)
open import Relation.Nullary using (¬_)

open import Data.Fin
open import Data.Nat
open import Data.Vec
  using (Vec; []; _∷_; map; tabulate; foldr; lookup; _∈_; here; there)
open import Data.Vec.Properties using (tabulate-∘; ∈-tabulate)

∨≡¬[¬∧¬] : ∀ 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

b⋁ : ∀ {n} → Vec Bool n → Bool
b⋁ = foldr (λ _ → Bool) _b∨_ false

b⋀ : ∀ {n} → Vec Bool n → Bool
b⋀ = foldr (λ _ → Bool) _b∧_ true

⋁≡¬⋀¬ : ∀ {n} (xs : Vec Bool n) → b⋁ xs ≡ not (b⋀ (map not xs))
⋁≡¬⋀¬ [] = refl
⋁≡¬⋀¬ (false ∷ xs) = ⋁≡¬⋀¬ xs
⋁≡¬⋀¬ (true ∷ xs) = refl

⋁≡¬⋀¬′ : ∀ {n} (f : Fin n → Bool) → b⋁ (tabulate f) ≡ not (b⋀ (tabulate (not ∘ f)))
⋁≡¬⋀¬′ f = trans (⋁≡¬⋀¬ (tabulate f)) (cong (not ∘ b⋀) (sym $ tabulate-∘ not f))

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-pair : ∀ {x y} → true ≡ x b∧ y → true ≡ x × true ≡ y
true-pair {false} {false} p = p , p
true-pair {false} {true} p = p , refl
true-pair {true} {false} p = refl , p
true-pair {true} {true} p = p , p

true-product :
  ∀ {n} {xs : Vec Bool n} → true ≡ b⋀ xs → {x : Bool} → (x ∈ xs) → true ≡ x
true-product eq {x} here = proj₁ (true-pair {x} eq)
true-product {xs = y ∷ _} eq (there elem) =
  true-product (proj₂ (true-pair {y} eq)) elem

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

false-sum : ∀ {x y} → false ≡ x b∧ y → false ≡ x ⊎ false ≡ y
false-sum {false} {false} eq = inj₁ eq
false-sum {false} {true} eq = inj₁ refl
false-sum {true} {false} eq = inj₂ refl
false-sum {true} {true} eq = inj₁ eq

false≢true : ¬ false ≡ true
false≢true eq = subst (T ∘ not) eq tt

false-∈ :
  ∀ {n} {xs : Vec Bool n} → false ≡ b⋀ xs → false ∈ xs
false-∈ {xs = []} eq = ⊥-elim (false≢true eq)
false-∈ {xs = x ∷ xs} eq =
  case false-sum {x} eq of λ
  { (inj₁ this) → subst (λ y → false ∈ y ∷ xs) this here
  ; (inj₂ those) → there (false-∈ those)
  }

tabulate-argument :
  ∀ {a n} {A : Set a} {x : A} (f : Fin n → A) → x ∈ tabulate f → ∃ λ i → x ≡ f i
tabulate-argument f here = zero , refl
tabulate-argument f (there p) with tabulate-argument (f ∘ suc) p
tabulate-argument f (there p) | i , eq = suc i , eq


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)

join : ∀ {a} {A : Set a} → ¬ ¬ ¬ ¬ A → ¬ ¬ A
join = ¬¬¬-elim

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

¬¬-map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → ¬ ¬ A → ¬ ¬ B
¬¬-map f ¬¬a ¬b = ¬¬a (¬b ∘ f)

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 A→¬¬B = join (¬¬-map A→¬¬B ¬¬A)

¬[¬×¬]→¬¬⊎ : ∀ {a b} {A : Set a} {B : Set b} → ¬ (¬ A × ¬ B) → ¬ ¬ (A ⊎ B)
¬[¬×¬]→¬¬⊎ {A = A} {B} p ¬⊎ = p (¬⊎ ∘ inj₁ , ¬⊎ ∘ inj₂)

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

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

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

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

example :
  ∀ {a b} {A : Set a} {B : A → Set b} →
  ¬ ((x : A) → ¬ B x) → ¬ ¬ ∃ λ x → B x
example = contrapositive (λ f a b → f (a , b))

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

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

¬[׬]→¬¬→ : ∀ {a b} {A : Set a} {B : Set b} → ¬ (A × ¬ B) → ¬ ¬ (A → B)
¬[׬]→¬¬→ {A = A} {B = B} f = ¬¬-pull (λ a ¬b → f (a , ¬b))

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

counterexample :
  ∀ {a b} {A : Set a} {B : A → Set b} →
  ¬ ((x : A) → ¬ ¬ B x) → ¬ ¬ ∃ λ x → ¬ B x
counterexample ¬∀¬¬ ¬∃¬ = ¬∀¬¬ (¬∃→∀¬ ¬∃¬)
  where
  ¬∃→∀¬ : ∀ {a b} {A : Set a} {B : A → Set b} → ¬ ∃ B → (x : A) → ¬ B x
  ¬∃→∀¬ f a b = f (a , b)

¬¬-push-dep :
  ∀ {a b} {A : Set a} {B : A → Set b} →
  ¬ ¬ ((x : A) → B x) → ((x : A) → ¬ ¬ B x)
¬¬-push-dep ¬¬f a = ¬¬f >>= λ f → pure (f a)

module Propositional where

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

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

  interpret : ∀ {A} → (A → Bool) → Term 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)

  Term→Set : ∀ {A} → (A → Set) → Term A → Set
  Term→Set f (var x) = f x
  Term→Set f true = ⊤
  Term→Set f false = ⊥
  Term→Set f (! t) = ¬ Term→Set f t
  Term→Set f (t ∨ u) = Term→Set f t ⊎ Term→Set f u
  Term→Set f (t ∧ u) = Term→Set f t × Term→Set f u
  Term→Set f (t ⇒ u) = Term→Set f t → Term→Set f u
  Term→Set f (t ⇔ u) = Term→Set f t ↔ Term→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} → Term 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)

  simplify-correct :
    ∀ {A} (f : A → Bool) (t : Term 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)))

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

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

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

  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 =
    let tp , up = true-pair {sinterpret f t} p in
    sembed f t tp >>= λ ts →
    sembed f u up >>= λ 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 : Term A) →
    true ≡ interpret f t → ¬ ¬ Term→Set (_≡_ true ∘ f) t
  embed f t p =
    sembed f (simplify t) (trans p (simplify-correct f t)) >>= λ ss →
    SimpleSet→¬¬TermSet f t ss

module FirstOrder where
  infixr 6 !_
  infixr 5 _∨_ _∧_
  infixr 4 _⇒_ _⇔_

  data Term (A : Set) (n : A → ℕ) (Γ : ℕ) : Set where
    prop : (a : A) (vs : Vec (Fin Γ) (n a)) → Term A n Γ
    true false : Term A n Γ
    !_ : Term A n Γ → Term A n Γ
    _∨_ _∧_ _⇒_ _⇔_ : (t u : Term A n Γ) → Term A n Γ
    ⋁ ⋀ : Term A n (suc Γ) → Term A n Γ

  interpret :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ) (f : (a : A) → Vec (Fin D) (n a) → Bool) →
    Term A n Γ → Bool
  interpret ctx f (prop a vs) = f a (map (λ v → lookup v ctx) vs)
  interpret ctx f true = true
  interpret ctx f false = false
  interpret ctx f (! t) = not (interpret ctx f t)
  interpret ctx f (t ∨ u) = interpret ctx f t b∨ interpret ctx f u
  interpret ctx f (t ∧ u) = interpret ctx f t b∧ interpret ctx f u
  interpret ctx f (t ⇒ u) = not (interpret ctx f t) b∨ interpret ctx f u
  interpret ctx f (t ⇔ u) =
    let u′ = interpret ctx f u in
    if interpret ctx f t then u′ else not u′
  interpret ctx f (⋁ t) =
    foldr (λ _ → Bool) _b∨_ false (tabulate (λ c → interpret (c ∷ ctx) f t))
  interpret ctx f (⋀ t) =
    foldr (λ _ → Bool) _b∧_ true (tabulate (λ c → interpret (c ∷ ctx) f t))

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

  Term→Set :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ) (f : (a : A) → Vec (Fin D) (n a) → Set) →
    Term A n Γ → Set
  Term→Set ctx f (prop a vs) = f a (map (λ v → lookup v ctx) vs)
  Term→Set ctx f true = ⊤
  Term→Set ctx f false = ⊥
  Term→Set ctx f (! t) = ¬ Term→Set ctx f t
  Term→Set ctx f (t ∨ u) = ¬ (¬ Term→Set ctx f t × ¬ Term→Set ctx f u)
  Term→Set ctx f (t ∧ u) = Term→Set ctx f t × Term→Set ctx f u
  Term→Set ctx f (t ⇒ u) = Term→Set ctx f t → ¬ ¬ Term→Set ctx f u
  Term→Set ctx f (t ⇔ u) = (¬ ¬ Term→Set ctx f t) ↔ (¬ ¬ Term→Set ctx f u)
  Term→Set ctx f (⋁ t) = ¬ ∀ c → ¬ Term→Set (c ∷ ctx) f t
  Term→Set ctx f (⋀ t) = ∀ c → Term→Set (c ∷ ctx) f t

  infixr 6 s!_
  infixr 5 _s∧_

  data SimpleTerm (A : Set) (n : A → ℕ) (Γ : ℕ) : Set where
    sprop : (a : A) → Vec (Fin Γ) (n a) → SimpleTerm A n Γ
    strue sfalse : SimpleTerm A n Γ
    s!_ : SimpleTerm A n Γ → SimpleTerm A n Γ
    _s∧_ : (t u : SimpleTerm A n Γ) → SimpleTerm A n Γ
    s⋀ : SimpleTerm A n (suc Γ) → SimpleTerm A n Γ

  sinterpret :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ) (f : (a : A) → Vec (Fin D) (n a) → Bool) →
    SimpleTerm A n Γ → Bool
  sinterpret ctx f (sprop a vs) = f a (map (λ v → lookup v ctx) vs)
  sinterpret ctx f strue = true
  sinterpret ctx f sfalse = false
  sinterpret ctx f (s! t) = not (sinterpret ctx f t)
  sinterpret ctx f (t s∧ u) = sinterpret ctx f t b∧ sinterpret ctx f u
  sinterpret ctx f (s⋀ t) =
    foldr (λ _ → Bool) _b∧_ true (tabulate (λ c → sinterpret (c ∷ ctx) f t))

  Simple→Set :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ) (f : (a : A) → Vec (Fin D) (n a) → Set) →
    SimpleTerm A n Γ → Set
  Simple→Set ctx f (sprop a vs) = f a (map (λ v → lookup v ctx) vs)
  Simple→Set ctx f strue = ⊤
  Simple→Set ctx f sfalse = ⊥
  Simple→Set ctx f (s! t) = ¬ Simple→Set ctx f t
  Simple→Set ctx f (t s∧ u) = Simple→Set ctx f t × Simple→Set ctx f u
  Simple→Set ctx f (s⋀ t) = ∀ c → Simple→Set (c ∷ ctx) f t

  simplify : ∀ {A n Γ} → Term A n Γ → SimpleTerm A n Γ
  simplify (prop a vs) = sprop a vs
  simplify true = strue
  simplify false = sfalse
  simplify (! p) = s! simplify p
  simplify (p ∨ q) = s! (s! simplify p s∧ s! simplify q)
  simplify (p ∧ q) = simplify p s∧ simplify q
  simplify (p ⇒ q) = s! (simplify p s∧ s! simplify q)
  simplify (p ⇔ q) =
    let sp = simplify p in
    let sq = simplify q in
    s! (sp s∧ s! sq) s∧ s! (sq s∧ s! sp)
  simplify (⋁ p) = s! s⋀ (s! simplify p)
  simplify (⋀ p) = s⋀ (simplify p)

  postulate
    funext : ∀ {a b} {A : Set a} {B : Set b} {f g : A → B} →
             ((x : A) → f x ≡ g x) → f ≡ g

  simplify-correct :
    ∀ {A n Γ D} ctx → (f : (a : A) → Vec (Fin D) (n a) → Bool) (t : Term A n Γ) →
    interpret ctx f t ≡ sinterpret ctx f (simplify t)
  simplify-correct ctx f (prop a vs) = refl
  simplify-correct ctx f true = refl
  simplify-correct ctx f false = refl
  simplify-correct ctx f (! t) = cong not (simplify-correct ctx f t)
  simplify-correct ctx f (t ∨ u) =
    trans (cong₂ _b∨_ (simplify-correct ctx f t) (simplify-correct ctx f u))
          (∨≡¬[¬∧¬] (sinterpret ctx f (simplify t))
                    (sinterpret ctx f (simplify u)))
  simplify-correct ctx f (t ∧ u) =
    cong₂ _b∧_ (simplify-correct ctx f t) (simplify-correct ctx f u)
  simplify-correct ctx f (t ⇒ u) =
    trans (cong₂ (λ x y → not x b∨ y) (simplify-correct ctx f t)
                                      (simplify-correct ctx f u))
          (¬∨≡¬[∧¬] (sinterpret ctx f (simplify t))
                    (sinterpret ctx f (simplify u)))
  simplify-correct ctx f (t ⇔ u) =
    trans (cong₂ (λ x y → if x then y else not y) (simplify-correct ctx f t)
                                                  (simplify-correct ctx f u))
          (⇔-simplify (sinterpret ctx f (simplify t))
                      (sinterpret ctx f (simplify u)))
  simplify-correct ctx f (⋁ t) =
    trans (cong (foldr (λ _ → Bool) _b∨_ false ∘ tabulate)
                (funext λ c → simplify-correct (c ∷ ctx) f t))
          (⋁≡¬⋀¬′ (λ c → sinterpret (c ∷ ctx) f (simplify t)))
  simplify-correct ctx f (⋀ t) =
    cong (foldr (λ _ → Bool) _b∧_ true ∘ tabulate)
         (funext λ c → simplify-correct (c ∷ ctx) f t)

  ⌈_⌉ :
    ∀ {a b} {A : Set a} {B : A → Set b}
    (f : (x : A) → B x → Bool) → (y : A) → B y → Set
  ⌈ f ⌉ a b = true ≡ f a b

  SimpleSet→TermSet :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ)
    (f : (a : A) → Vec (Fin D) (n a) → Bool) (t : Term A n Γ) →
    Simple→Set ctx ⌈ f ⌉ (simplify t) → Term→Set ctx ⌈ f ⌉ t

  TermSet→SimpleSet :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ)
    (f : (a : A) → Vec (Fin D) (n a) → Bool) (t : Term A n Γ) →
    Term→Set ctx ⌈ f ⌉ t → Simple→Set ctx ⌈ f ⌉ (simplify t)

  SimpleSet→TermSet ctx f (prop a vs) s = s
  SimpleSet→TermSet ctx f true s = s
  SimpleSet→TermSet ctx f false s = s
  SimpleSet→TermSet ctx f (! t) ¬ts = ¬ts ∘ TermSet→SimpleSet ctx f t
  SimpleSet→TermSet ctx f (t ∨ u) s (¬tp , ¬up) =
    s (¬tp ∘ SimpleSet→TermSet ctx f t , ¬up ∘ SimpleSet→TermSet ctx f u)
  SimpleSet→TermSet ctx f (t ∧ u) (tp , up) =
    SimpleSet→TermSet ctx f t tp , SimpleSet→TermSet ctx f u up
  SimpleSet→TermSet ctx f (t ⇒ u) s tp ¬up =
    s (TermSet→SimpleSet ctx f t tp , ¬up ∘ SimpleSet→TermSet ctx f u)
  SimpleSet→TermSet ctx f (t ⇔ u) (rs , ls) =
    (λ ¬¬tp ¬up → ⊥-prop $
      ¬¬tp >>= λ tp →
      pure (rs (TermSet→SimpleSet ctx f t tp , ¬up ∘ SimpleSet→TermSet ctx f u))
    ) ,
    (λ ¬¬up ¬tp → ⊥-prop $
      ¬¬up >>= λ up →
      pure (ls (TermSet→SimpleSet ctx f u up , ¬tp ∘ SimpleSet→TermSet ctx f t))
    )
  SimpleSet→TermSet ctx f (⋁ t) s ¬tp =
    s (λ c → ¬tp c ∘ SimpleSet→TermSet (c ∷ ctx) f t)
  SimpleSet→TermSet ctx f (⋀ t) ts c = SimpleSet→TermSet (c ∷ ctx) f t (ts c)

  TermSet→SimpleSet ctx f (prop a vs) p = p
  TermSet→SimpleSet ctx f true p = p
  TermSet→SimpleSet ctx f false p = p
  TermSet→SimpleSet ctx f (! t) ¬tp = ¬tp ∘ SimpleSet→TermSet ctx f t
  TermSet→SimpleSet ctx f (t ∨ u) p (¬ts , ¬us) =
    p (¬ts ∘ TermSet→SimpleSet ctx f t , ¬us ∘ TermSet→SimpleSet ctx f u)
  TermSet→SimpleSet ctx f (t ∧ u) (tp , up) =
    TermSet→SimpleSet ctx f t tp , TermSet→SimpleSet ctx f u up
  TermSet→SimpleSet ctx f (t ⇒ u) p (ts , ¬us) = ⊥-prop $
    p (SimpleSet→TermSet ctx f t ts) >>= λ up →
    pure (¬us (TermSet→SimpleSet ctx f u up))
  TermSet→SimpleSet ctx f (t ⇔ u) (rp , lp) =
    (λ { (ts , ¬us) → ⊥-prop $
      rp (pure (SimpleSet→TermSet ctx f t ts)) >>= λ up →
      pure (¬us (TermSet→SimpleSet ctx f u up))
    }) ,
    (λ { (us , ¬ts) → ⊥-prop $
      lp (pure (SimpleSet→TermSet ctx f u us)) >>= λ tp →
      pure (¬ts (TermSet→SimpleSet ctx f t tp))
    })
  TermSet→SimpleSet ctx f (⋁ t) p =
    p ∘ (λ ¬ts c → ¬ts c ∘ TermSet→SimpleSet (c ∷ ctx) f t)
  TermSet→SimpleSet ctx f (⋀ t) tp c = TermSet→SimpleSet (c ∷ ctx) f t (tp c)

  ∈-index : ∀ {a n} {A : Set a} {x : A} {xs : Vec A n} → x ∈ xs → Fin n
  ∈-index here = zero
  ∈-index (there p) = suc (∈-index p)

  sembed :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ)
    (f : (a : A) → Vec (Fin D) (n a) → Bool) (t : SimpleTerm A n Γ) →
    true ≡ sinterpret ctx f t → Simple→Set ctx ⌈ f ⌉ t
  ¬sembed :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ)
    (f : (a : A) → Vec (Fin D) (n a) → Bool) (t : SimpleTerm A n Γ) →
    false ≡ sinterpret ctx f t → ¬ Simple→Set ctx ⌈ f ⌉ t

  sembed ctx f (sprop a vs) eq = eq
  sembed ctx f strue eq = tt
  sembed ctx f sfalse eq = subst T eq tt
  sembed ctx f (s! t) eq = ¬sembed ctx f t (trans (cong not eq) (not-not _))
  sembed ctx f (t s∧ u) eq =
    let teq , ueq = true-pair {sinterpret ctx f t} eq in
    sembed ctx f t teq , sembed ctx f u ueq
  sembed ctx f (s⋀ t) eq c =
    let eqs = true-product {xs = tabulate λ c′ → sinterpret (c′ ∷ ctx) f t} eq in
    sembed (c ∷ ctx) f t (eqs (∈-tabulate _ c))

  ¬sembed ctx f (sprop a x) eq ts = false≢true (trans eq (sym ts))
  ¬sembed ctx f strue eq ts = subst (T ∘ not) eq tt
  ¬sembed ctx f sfalse eq ts = ts
  ¬sembed ctx f (s! t) eq ts = ts (sembed ctx f t (trans (cong not eq) (not-not _)))
  ¬sembed ctx f (t s∧ u) eq (ts , us) =
    case false-sum {sinterpret ctx f t} eq of λ
    { (inj₁ teq) → ¬sembed ctx f t teq ts
    ; (inj₂ ueq) → ¬sembed ctx f u ueq us
    }
  ¬sembed ctx f (s⋀ t) eq ts with tabulate-argument (λ c → sinterpret (c ∷ ctx) f t) (false-∈ eq)
  ¬sembed ctx f (s⋀ t) eq ts | c , ceq = ¬sembed (c ∷ ctx) f t ceq (ts c)

  embed :
    ∀ {A n Γ D} (ctx : Vec (Fin D) Γ)
    (f : (a : A) → Vec (Fin D) (n a) → Bool) (t : Term A n Γ) →
    true ≡ interpret ctx f t → Term→Set ctx ⌈ f ⌉ t
  embed ctx f t p =
    SimpleSet→TermSet ctx f t (sembed ctx f (simplify t)
                      (trans p (simplify-correct ctx f t)))