open import 1Lab.Prelude
open import Data.Bool
open import Data.Fin
open import Data.List
open import Data.Nat
module Data.Bool.CNF where
private variable
n : Nat
data Expr (n : Nat) : Type where
evar : Fin n → Expr n
etrue : Expr n
efalse : Expr n
enot : Expr n → Expr n
eand : Expr n → Expr n → Expr n
eor : Expr n → Expr n → Expr n
⟦_⟧ᵉ : Expr n → (Fin n → Bool) → Bool
⟦ evar x ⟧ᵉ ρ = ρ x
⟦ etrue ⟧ᵉ ρ = true
⟦ efalse ⟧ᵉ ρ = false
⟦ enot e ⟧ᵉ ρ = not (⟦ e ⟧ᵉ ρ)
⟦ eand e1 e2 ⟧ᵉ ρ = and (⟦ e1 ⟧ᵉ ρ) (⟦ e2 ⟧ᵉ ρ)
⟦ eor e1 e2 ⟧ᵉ ρ = or (⟦ e1 ⟧ᵉ ρ) (⟦ e2 ⟧ᵉ ρ)
data Atom (n : Nat) : Type where
avar : Fin n → Atom n
anegvar : Fin n → Atom n
Clause : Nat → Type
Clause n = List (Atom n)
CNF : Nat → Type
CNF n = List (Clause n)
⟦_⟧ᵃ : Atom n → (Fin n → Bool) → Bool
⟦ avar x ⟧ᵃ ρ = ρ x
⟦ anegvar x ⟧ᵃ ρ = not (ρ x)
⟦_⟧ᶜ : Clause n → (Fin n → Bool) → Bool
⟦ [] ⟧ᶜ ρ = false
⟦ a ∷ as ⟧ᶜ ρ = or (⟦ a ⟧ᵃ ρ) (⟦ as ⟧ᶜ ρ)
⟦_⟧ⁿ : CNF n → (Fin n → Bool) → Bool
⟦ [] ⟧ⁿ ρ = true
⟦ c ∷ cs ⟧ⁿ ρ = and (⟦ c ⟧ᶜ ρ) (⟦ cs ⟧ⁿ ρ)
atom-not : Atom n → Atom n
atom-not (avar x) = anegvar x
atom-not (anegvar x) = avar x
clause-or : Clause n → Clause n → Clause n
clause-or as bs = as ++ bs
clause-not : Clause n → CNF n
clause-not [] = []
clause-not (a ∷ as) = (atom-not a ∷ []) ∷ clause-not as
cnf-var : Fin n → CNF n
cnf-var n = (avar n ∷ []) ∷ []
cnf-true : CNF n
cnf-true = []
cnf-false : CNF n
cnf-false = [] ∷ []
cnf-and : CNF n → CNF n → CNF n
cnf-and as bs = as ++ bs
cnf-or : CNF n → CNF n → CNF n
cnf-or [] bs = cnf-true
cnf-or (a ∷ as) bs = cnf-and (map (clause-or a) bs) (cnf-or as bs)
cnf-not : CNF n → CNF n
cnf-not [] = cnf-false
cnf-not (a ∷ as) = cnf-or (clause-not a) (cnf-not as)
eval : Expr n → CNF n
eval (evar x) = cnf-var x
eval etrue = cnf-true
eval efalse = cnf-false
eval (enot e) = cnf-not (eval e)
eval (eand e1 e2) = cnf-and (eval e1) (eval e2)
eval (eor e1 e2) = cnf-or (eval e1) (eval e2)
reflect-atom : Atom n → Expr n
reflect-atom (avar x) = evar x
reflect-atom (anegvar x) = enot (evar x)
reflect-clause : Clause n → Expr n
reflect-clause = foldr (λ a → eor (reflect-atom a)) efalse
reflect : CNF n → Expr n
reflect = foldr (λ c → eand (reflect-clause c)) etrue
nf : Expr n → Expr n
nf e = reflect (eval e)
atom-not-sound : ∀ (a : Atom n) → (ρ : Fin n → Bool)
→ ⟦ atom-not a ⟧ᵃ ρ ≡ not (⟦ a ⟧ᵃ ρ)
atom-not-sound (avar x) ρ = refl
atom-not-sound (anegvar x) ρ = sym $ not-involutive (ρ x)
clause-or-sound : ∀ (as bs : Clause n) → (ρ : Fin n → Bool)
→ ⟦ clause-or as bs ⟧ᶜ ρ ≡ or (⟦ as ⟧ᶜ ρ) (⟦ bs ⟧ᶜ ρ)
clause-or-sound [] bs ρ = refl
clause-or-sound (a ∷ as) bs ρ =
or (⟦ a ⟧ᵃ ρ) (⟦ as ++ bs ⟧ᶜ ρ) ≡⟨ ap (or (⟦ a ⟧ᵃ ρ)) (clause-or-sound as bs ρ) ⟩
or (⟦ a ⟧ᵃ ρ) (or (⟦ as ⟧ᶜ ρ) (⟦ bs ⟧ᶜ ρ)) ≡⟨ or-associative (⟦ a ⟧ᵃ ρ) (⟦ as ⟧ᶜ ρ) (⟦ bs ⟧ᶜ ρ) ⟩
or (or (⟦ a ⟧ᵃ ρ) (⟦ as ⟧ᶜ ρ)) (⟦ bs ⟧ᶜ ρ) ∎
cnf-and-sound : ∀ (as bs : CNF n) → (ρ : Fin n → Bool)
→ ⟦ cnf-and as bs ⟧ⁿ ρ ≡ and (⟦ as ⟧ⁿ ρ) (⟦ bs ⟧ⁿ ρ)
cnf-and-sound [] bs ρ = refl
cnf-and-sound (b ∷ as) bs ρ =
and (⟦ b ⟧ᶜ ρ) (⟦ as ++ bs ⟧ⁿ ρ) ≡⟨ ap (and (⟦ b ⟧ᶜ ρ)) (cnf-and-sound as bs ρ) ⟩
and (⟦ b ⟧ᶜ ρ) (and (⟦ as ⟧ⁿ ρ) (⟦ bs ⟧ⁿ ρ)) ≡⟨ and-associative (⟦ b ⟧ᶜ ρ) (⟦ as ⟧ⁿ ρ) (⟦ bs ⟧ⁿ ρ) ⟩
and (and (⟦ b ⟧ᶜ ρ) (⟦ as ⟧ⁿ ρ)) (⟦ bs ⟧ⁿ ρ) ∎
map-clause-or-sound : ∀ (a : Clause n) (bs : CNF n) → (ρ : Fin n → Bool)
→ ⟦ map (clause-or a) bs ⟧ⁿ ρ ≡ or (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)
map-clause-or-sound a [] ρ = sym $ or-truer _
map-clause-or-sound a (b ∷ bs) ρ =
and (⟦ clause-or a b ⟧ᶜ ρ) (⟦ map (clause-or a) bs ⟧ⁿ ρ) ≡⟨ ap (and (⟦ clause-or a b ⟧ᶜ ρ)) (map-clause-or-sound a bs ρ) ⟩
and (⟦ clause-or a b ⟧ᶜ ρ) (or (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ≡⟨ and-distrib-orl (⟦ clause-or a b ⟧ᶜ ρ) (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ) ⟩
or (and ⌜ ⟦ clause-or a b ⟧ᶜ ρ ⌝ (⟦ a ⟧ᶜ ρ)) (and (⟦ clause-or a b ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ≡⟨ ap! (clause-or-sound a b ρ) ⟩
or ⌜ and (or (⟦ a ⟧ᶜ ρ) (⟦ b ⟧ᶜ ρ)) (⟦ a ⟧ᶜ ρ) ⌝ (and (⟦ clause-or a b ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ≡⟨ ap! (and-commutative (or (⟦ a ⟧ᶜ ρ) (⟦ b ⟧ᶜ ρ)) (⟦ a ⟧ᶜ ρ) ∙ and-absorbs-orr (⟦ a ⟧ᶜ ρ) (⟦ b ⟧ᶜ ρ)) ⟩
or (⟦ a ⟧ᶜ ρ) (and ⌜ ⟦ clause-or a b ⟧ᶜ ρ ⌝ (⟦ bs ⟧ⁿ ρ)) ≡⟨ ap! (clause-or-sound a b ρ) ⟩
or (⟦ a ⟧ᶜ ρ) ⌜ and (or (⟦ a ⟧ᶜ ρ) (⟦ b ⟧ᶜ ρ)) (⟦ bs ⟧ⁿ ρ) ⌝ ≡⟨ ap! (and-distrib-orr (⟦ a ⟧ᶜ ρ) (⟦ b ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ⟩
or (⟦ a ⟧ᶜ ρ) (or (and (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) (and (⟦ b ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ))) ≡⟨ or-associative (⟦ a ⟧ᶜ ρ) (and (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) (and (⟦ b ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ⟩
or ⌜ or (⟦ a ⟧ᶜ ρ) (and (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ⌝ (and (⟦ b ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ≡⟨ ap! (or-absorbs-andr (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ⟩
or (⟦ a ⟧ᶜ ρ) (and (⟦ b ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ∎
cnf-or-sound : ∀ (as bs : CNF n) → (ρ : Fin n → Bool)
→ ⟦ cnf-or as bs ⟧ⁿ ρ ≡ or (⟦ as ⟧ⁿ ρ) (⟦ bs ⟧ⁿ ρ)
cnf-or-sound [] bs ρ = refl
cnf-or-sound (a ∷ as) bs ρ =
⟦ cnf-and (map (clause-or a) bs) (cnf-or as bs) ⟧ⁿ ρ ≡⟨ cnf-and-sound (map (clause-or a) bs) (cnf-or as bs) ρ ⟩
and ⌜ ⟦ map (clause-or a) bs ⟧ⁿ ρ ⌝ (⟦ cnf-or as bs ⟧ⁿ ρ) ≡⟨ ap! (map-clause-or-sound a bs ρ) ⟩
and (or (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) ⌜ ⟦ cnf-or as bs ⟧ⁿ ρ ⌝ ≡⟨ ap! (cnf-or-sound as bs ρ) ⟩
and (or (⟦ a ⟧ᶜ ρ) (⟦ bs ⟧ⁿ ρ)) (or (⟦ as ⟧ⁿ ρ) (⟦ bs ⟧ⁿ ρ)) ≡˘⟨ or-distrib-andr (⟦ a ⟧ᶜ ρ) (⟦ as ⟧ⁿ ρ) (⟦ bs ⟧ⁿ ρ) ⟩
or (⟦ a ∷ as ⟧ⁿ ρ) (⟦ bs ⟧ⁿ ρ) ∎
clause-not-sound : ∀ (as : Clause n) → (ρ : Fin n → Bool)
→ ⟦ clause-not as ⟧ⁿ ρ ≡ not (⟦ as ⟧ᶜ ρ)
clause-not-sound [] ρ = refl
clause-not-sound (a ∷ as) ρ =
and (or (⟦ atom-not a ⟧ᵃ ρ) false) (⟦ clause-not as ⟧ⁿ ρ) ≡⟨ ap (λ ϕ → and ϕ (⟦ clause-not as ⟧ⁿ ρ)) (or-falser (⟦ atom-not a ⟧ᵃ ρ)) ⟩
and (⟦ atom-not a ⟧ᵃ ρ) (⟦ clause-not as ⟧ⁿ ρ) ≡⟨ ap₂ and (atom-not-sound a ρ) (clause-not-sound as ρ) ⟩
and (not (⟦ a ⟧ᵃ ρ)) (not (⟦ as ⟧ᶜ ρ)) ≡˘⟨ not-or≡and-not (⟦ a ⟧ᵃ ρ) (⟦ as ⟧ᶜ ρ) ⟩
not (⟦ a ∷ as ⟧ᶜ ρ) ∎
cnf-not-sound : ∀ (as : CNF n) → (ρ : Fin n → Bool)
→ ⟦ cnf-not as ⟧ⁿ ρ ≡ not (⟦ as ⟧ⁿ ρ)
cnf-not-sound [] ρ = refl
cnf-not-sound (a ∷ as) ρ =
⟦ cnf-or (clause-not a) (cnf-not as) ⟧ⁿ ρ ≡⟨ cnf-or-sound (clause-not a) (cnf-not as) ρ ⟩
or ⌜ ⟦ clause-not a ⟧ⁿ ρ ⌝ (⟦ cnf-not as ⟧ⁿ ρ) ≡⟨ ap₂ or (clause-not-sound a ρ) (cnf-not-sound as ρ) ⟩
or (not (⟦ a ⟧ᶜ ρ)) (not (⟦ as ⟧ⁿ ρ)) ≡˘⟨ not-and≡or-not (⟦ a ⟧ᶜ ρ) (⟦ as ⟧ⁿ ρ) ⟩
not (and (⟦ a ⟧ᶜ ρ) (⟦ as ⟧ⁿ ρ)) ∎
cnf-var-sound : ∀ (x : Fin n) → (ρ : Fin n → Bool)
→ ⟦ cnf-var x ⟧ⁿ ρ ≡ ρ x
cnf-var-sound x ρ =
and (or (ρ x) false) true ≡⟨ and-truer (or (ρ x) false) ⟩
or (ρ x) false ≡⟨ or-falser (ρ x) ⟩
ρ x ∎
eval-sound : ∀ (e : Expr n) → (ρ : Fin n → Bool)
→ ⟦ eval e ⟧ⁿ ρ ≡ ⟦ e ⟧ᵉ ρ
eval-sound (evar x) ρ = cnf-var-sound x ρ
eval-sound etrue ρ = refl
eval-sound efalse ρ = refl
eval-sound (enot e) ρ =
⟦ cnf-not (eval e) ⟧ⁿ ρ ≡⟨ cnf-not-sound (eval e) ρ ⟩
not (⟦ eval e ⟧ⁿ ρ) ≡⟨ ap not (eval-sound e ρ) ⟩
not (⟦ e ⟧ᵉ ρ) ∎
eval-sound (eand e1 e2) ρ =
⟦ cnf-and (eval e1) (eval e2) ⟧ⁿ ρ ≡⟨ cnf-and-sound (eval e1) (eval e2) ρ ⟩
and (⟦ eval e1 ⟧ⁿ ρ) (⟦ eval e2 ⟧ⁿ ρ) ≡⟨ ap₂ and (eval-sound e1 ρ) (eval-sound e2 ρ) ⟩
and (⟦ e1 ⟧ᵉ ρ) (⟦ e2 ⟧ᵉ ρ) ∎
eval-sound (eor e1 e2) ρ =
⟦ cnf-or (eval e1) (eval e2) ⟧ⁿ ρ ≡⟨ cnf-or-sound (eval e1) (eval e2) ρ ⟩
or (⟦ eval e1 ⟧ⁿ ρ) (⟦ eval e2 ⟧ⁿ ρ) ≡⟨ ap₂ or (eval-sound e1 ρ) (eval-sound e2 ρ) ⟩
or (⟦ e1 ⟧ᵉ ρ) (⟦ e2 ⟧ᵉ ρ) ∎reflect-atom-sound : ∀ (a : Atom n) → (ρ : Fin n → Bool)
→ ⟦ reflect-atom a ⟧ᵉ ρ ≡ ⟦ a ⟧ᵃ ρ
reflect-atom-sound (avar x) ρ = refl
reflect-atom-sound (anegvar x) ρ = refl
reflect-clause-sound : ∀ (as : Clause n) → (ρ : Fin n → Bool)
→ ⟦ reflect-clause as ⟧ᵉ ρ ≡ ⟦ as ⟧ᶜ ρ
reflect-clause-sound [] ρ = refl
reflect-clause-sound (a ∷ as) ρ =
ap₂ or (reflect-atom-sound a ρ) (reflect-clause-sound as ρ)
reflect-sound : ∀ (cs : CNF n) → (ρ : Fin n → Bool)
→ ⟦ reflect cs ⟧ᵉ ρ ≡ ⟦ cs ⟧ⁿ ρ
reflect-sound [] ρ = refl
reflect-sound (c ∷ cs) ρ =
ap₂ and (reflect-clause-sound c ρ) (reflect-sound cs ρ)nf-sound : ∀ (e : Expr n) → (ρ : Fin n → Bool)
→ ⟦ nf e ⟧ᵉ ρ ≡ ⟦ e ⟧ᵉ ρ
nf-sound e ρ = reflect-sound (eval e) ρ ∙ eval-sound e ρ