open import 1Lab.Prelude

open import Data.Bool
open import Data.List hiding (_++_)
open import Data.Dec
open import Data.Fin using (Fin; fzero; fsuc; avoid)
open import Data.Nat
open import Data.Sum

open import Logic.Propositional.Classical

open import Meta.Invariant
open import Meta.Brackets

import Data.List as List

module Logic.Propositional.Classical.CNF where

Conjunctive normal formsπŸ”—

As a general theme, it is often very useful to have some notion of normal-form for logical and algebraic expressions, and Classical propositional logic is no different! There are multiple possible choices of normal form, but we will be focusing on conjunctive normal form, or CNF for short.

A statement in propositional logic is in conjunctive normal form if it is written as a conjunction of disjunctions of (potentially negated) atoms. As an example, something like is in conjunctive normal form, yet something like is not.

We call the potentially negated atoms in a CNF expression literals, and the disjunctions clauses.

data Literal (Ξ“ : Nat) : Type where
  lit : Fin Ξ“ β†’ Literal Ξ“
  neg : Fin Ξ“ β†’ Literal Ξ“

Clause : (Ξ“ : Nat) β†’ Type
Clause Ξ“ = List (Literal Ξ“)

CNF : (Ξ“ : Nat) β†’ Type
CNF Ξ“ = List (Clause Ξ“)

private variable
  Ξ“ Ξ” Θ : Nat
  ψ ΞΈ ΞΆ : Ctx Ξ“
  P Q R : Proposition Ξ“

litβ‰ neg : βˆ€ {x y : Fin Ξ“} β†’ lit x ≑ neg y β†’ βŠ₯
lit≠neg {Γ = Γ} p = subst is-lit p tt where
  is-lit : Literal Ξ“ β†’ Type
  is-lit (lit x) = ⊀
  is-lit (neg x) = βŠ₯

lit-var : Literal Ξ“ β†’ Fin Ξ“
lit-var (lit x) = x
lit-var (neg x) = x

lit-val : Literal Ξ“ β†’ Bool
lit-val (lit x) = true
lit-val (neg x) = false

lit-inj : βˆ€ {x y : Fin Ξ“} β†’ lit x ≑ lit y β†’ x ≑ y
lit-inj p = ap lit-var p

neg-inj : βˆ€ {x y : Fin Ξ“} β†’ neg x ≑ neg y β†’ x ≑ y
neg-inj p = ap lit-var p

instance
  Discrete-Literal : Discrete (Literal Ξ“)
  Discrete-Literal {x = lit x} {lit y} = invmap (ap lit) lit-inj (x ≑? y)
  Discrete-Literal {x = lit x} {neg y} = no lit≠neg
  Discrete-Literal {x = neg x} {lit y} = no (litβ‰ neg ∘ sym)
  Discrete-Literal {x = neg x} {neg y} = invmap (ap neg) neg-inj (x ≑? y)

avoid-lit : (i : Fin (suc Ξ“)) (x : Literal (suc Ξ“)) β†’ Β¬ i ≑ lit-var x β†’ Literal Ξ“
avoid-lit i (lit x) p = lit (avoid i x p)
avoid-lit i (neg x) p = neg (avoid i x p)

SemanticsπŸ”—

Like their non-normal form brethren, expressions in CNF have a natural semantics in booleans. However, evaluation is particularly easy!

lit-sem : Literal Ξ“ β†’ (Fin Ξ“ β†’ Bool) β†’ Bool
lit-sem (lit x) ρ = ρ x
lit-sem (neg x) ρ = not (ρ x)

clause-sem : Clause Ξ“ β†’ (Fin Ξ“ β†’ Bool) β†’ Bool
clause-sem Ps ρ = any-of (Ξ» a β†’ lit-sem a ρ) Ps

cnf-sem : CNF Ξ“ β†’ (Fin Ξ“ β†’ Bool) β†’ Bool
cnf-sem Ps ρ = all-of (Ξ» d β†’ clause-sem d ρ) Ps

instance
  ⟦⟧-Literal : ⟦⟧-notation (Literal Ξ“)
  ⟦⟧-Literal {Ξ“ = Ξ“} = brackets ((Fin Ξ“ β†’ Bool) β†’ Bool) lit-sem

  ⟦⟧-Clause : ⟦⟧-notation (Clause Ξ“)
  ⟦⟧-Clause {Ξ“ = Ξ“} = brackets ((Fin Ξ“ β†’ Bool) β†’ Bool) clause-sem

  ⟦⟧-CNF : ⟦⟧-notation (CNF Ξ“)
  ⟦⟧-CNF {Ξ“ = Ξ“} = brackets ((Fin Ξ“ β†’ Bool) β†’ Bool) cnf-sem

SoundnessπŸ”—

We can extend the normal operations on propositions to expressions in CNF.

Atoms are represented by a single clause.

cnf-atom : Fin Ξ“ β†’ CNF Ξ“
cnf-atom x = (lit x ∷ []) ∷ []

True and false are represented by an expression with no clauses, and an expression with a single empty clause, respectively.

⊀cnf : CNF Ξ“
⊀cnf = []

βŠ₯cnf : CNF Ξ“
βŠ₯cnf = [] ∷ []

Conjunction can be defined by appending lists.

_∧cnf_ : CNF Ξ“ β†’ CNF Ξ“ β†’ CNF Ξ“
xs ∧cnf ys = xs List.++ ys

Disjunction is somewhat tricky, but can be handled by distributing each clause.

cnf-distrib : Clause Ξ“ β†’ CNF Ξ“ β†’ CNF Ξ“
cnf-distrib P Q = map (P List.++_) Q

_∨cnf_ : CNF Ξ“ β†’ CNF Ξ“ β†’ CNF Ξ“
[]       ∨cnf Q = []
(P ∷ Ps) ∨cnf Q = cnf-distrib P Q ∧cnf (Ps ∨cnf Q)

Negation is performed by negating all the clauses, and then taking the disjunction of the negated clauses.

Β¬lit : Literal Ξ“ β†’ Literal Ξ“
Β¬lit (lit x) = neg x
Β¬lit (neg x) = lit x

Β¬clause : Clause Ξ“ β†’ CNF Ξ“
Β¬clause P = map (Ξ» a β†’ Β¬lit a ∷ []) P

Β¬cnf : CNF Ξ“ β†’ CNF Ξ“
Β¬cnf []      = βŠ₯cnf
¬cnf (P ∷ Q) = ¬clause P ∨cnf ¬cnf Q
All of these operations commute with interpretation in the expected way, but showing this requires a few nightmare inductive arguments over syntax. 
cnf-atom-sound : βˆ€ (x : Fin Ξ“) (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ cnf-atom x ⟧ ρ ≑ ρ x
cnf-atom-sound x ρ = and-truer _ βˆ™ or-falser _

βŠ₯cnf-sound : βˆ€ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ βŠ₯cnf ⟧ ρ ≑ false
βŠ₯cnf-sound ρ = refl

⊀cnf-sound : βˆ€ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ ⊀cnf ⟧ ρ ≑ true
⊀cnf-sound ρ = refl

∧cnf-sound : βˆ€ (P Q : CNF Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ P ∧cnf Q ⟧ ρ ≑ and (⟦ P ⟧ ρ) (⟦ Q ⟧ ρ)
∧cnf-sound P Q ρ = all-of-++ (any-of (Ξ» a β†’ lit-sem a ρ)) P Q

cnf-distrib-sound
  : (P : Clause Ξ“) (Q : CNF Ξ“)
  β†’ (ρ : Fin Ξ“ β†’ Bool)
  β†’ ⟦ cnf-distrib P Q ⟧ ρ ≑ or (⟦ P ⟧ ρ) (⟦ Q ⟧ ρ)
cnf-distrib-sound []       Q ρ = ap (all-of (Ξ» d β†’ clause-sem d ρ)) (map-id Q)
cnf-distrib-sound (P ∷ Ps) Q ρ =
  all-of (Ξ» d β†’ ⟦ d ⟧ ρ) (map (Ξ» ys β†’ P ∷ (Ps List.++ ys)) Q) β‰‘βŸ¨ all-of-map _ _ Q βŸ©β‰‘
  all-of (Ξ» d β†’ ⟦ P ∷ (Ps List.++ d) ⟧ ρ) Q                   β‰‘βŸ¨ ap (Ξ» Ο• β†’ all-of Ο• Q) (funext Ξ» d β†’ any-of-++ _ (P ∷ Ps) d) βŸ©β‰‘
  all-of (Ξ» d β†’ or (⟦ P ∷ Ps ⟧ ρ) (⟦ d ⟧ ρ)) Q                β‰‘βŸ¨ all-of-or (Ξ» d β†’ ⟦ d ⟧ ρ) (⟦ P ∷ Ps ⟧ ρ) Q βŸ©β‰‘
  or (⟦ P ∷ Ps ⟧ ρ) (⟦ Q ⟧ ρ)                                 ∎

∨cnf-sound : βˆ€ (P Q : CNF Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ P ∨cnf Q ⟧ ρ ≑ or (⟦ P ⟧ ρ) (⟦ Q ⟧ ρ)
∨cnf-sound []       Q ρ = refl
∨cnf-sound (P ∷ Ps) Q ρ =
  ⟦ (P ∷ Ps) ∨cnf Q ⟧ ρ                                    β‰‘βŸ¨ all-of-++ (Ξ» d β†’ clause-sem d ρ) (cnf-distrib P Q) (Ps ∨cnf Q) βŸ©β‰‘
  and (⟦ cnf-distrib P Q ⟧ ρ) (⟦ Ps ∨cnf Q ⟧ ρ)            β‰‘βŸ¨ apβ‚‚ and (cnf-distrib-sound P Q ρ) (∨cnf-sound Ps Q ρ) βŸ©β‰‘
  and (or (⟦ P ⟧ ρ) (⟦ Q ⟧ ρ)) (or (⟦ Ps ⟧ ρ) (⟦ Q ⟧ ρ))   β‰‘Λ˜βŸ¨ or-distrib-andr (⟦ P ⟧ ρ) (⟦ Ps ⟧ ρ) (⟦ Q ⟧ ρ) βŸ©β‰‘Λ˜
  or (⟦ P ∷ Ps ⟧ ρ) (⟦ Q ⟧ ρ) ∎

Β¬lit-sound : (a : Literal Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ Β¬lit a ⟧ ρ ≑ not (⟦ a ⟧ ρ)
¬lit-sound (lit x) ρ = refl
¬lit-sound (neg x) ρ = sym (not-involutive (ρ x))

Β¬clause-sound : βˆ€ (P : Clause Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ Β¬clause P ⟧ ρ ≑ not (⟦ P ⟧ ρ)
¬clause-sound P ρ =
  all-of (Ξ» d β†’ ⟦ d ⟧ ρ) (map (Ξ» a β†’ Β¬lit a ∷ []) P)  β‰‘βŸ¨ all-of-map (Ξ» d β†’ ⟦ d ⟧ ρ) (Ξ» a β†’ Β¬lit a ∷ []) P βŸ©β‰‘
  all-of (Ξ» a β†’ or (⟦ Β¬lit a ⟧ ρ) false) P            β‰‘βŸ¨ ap (Ξ» Ο• β†’ all-of Ο• P) (funext Ξ» a β†’ or-falser (⟦ Β¬lit a ⟧ ρ)) βŸ©β‰‘
  all-of (Ξ» a β†’ ⟦ Β¬lit a ⟧ ρ) P                       β‰‘βŸ¨ ap (Ξ» Ο• β†’ all-of Ο• P) (funext Ξ» a β†’ Β¬lit-sound a ρ) βŸ©β‰‘
  all-of (Ξ» a β†’ not (⟦ a ⟧ ρ)) P                      β‰‘Λ˜βŸ¨ not-any-of (Ξ» a β†’ ⟦ a ⟧ ρ) P βŸ©β‰‘Λ˜
  not (⟦ P ⟧ ρ)                                       ∎

Β¬cnf-sound : βˆ€ (P : CNF Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ Β¬cnf P ⟧ ρ ≑ not (⟦ P ⟧ ρ)
¬cnf-sound []       ρ = refl
¬cnf-sound (P ∷ Ps) ρ =
  ⟦ (Β¬clause P ∨cnf Β¬cnf Ps) ⟧ ρ        β‰‘βŸ¨ ∨cnf-sound (Β¬clause P) (Β¬cnf Ps) ρ βŸ©β‰‘
  or (⟦ Β¬clause P ⟧ ρ) (⟦ Β¬cnf Ps ⟧ ρ)  β‰‘βŸ¨ apβ‚‚ or (Β¬clause-sound P ρ) (Β¬cnf-sound Ps ρ) βŸ©β‰‘
  or (not (⟦ P ⟧ ρ)) (not (⟦ Ps ⟧ ρ))   β‰‘Λ˜βŸ¨ not-and≑or-not (⟦ P  ⟧ ρ) (⟦ Ps ⟧ ρ) βŸ©β‰‘Λ˜
  not (⟦ P ∷ Ps ⟧ ρ)                    ∎

A naive algorithmπŸ”—

Armed with these operations on CNFs, we can give a translation from propositions into CNF. However, note that this is extremely naive, and will result in huge clause sizes! This is due to the fact that disjunction and negation distribute clauses, which will result in potentially exponential blow-ups in expression sizes.

cnf : Proposition Ξ“ β†’ CNF Ξ“
cnf (atom x)  = cnf-atom x
cnf β€œβŠ€β€       = ⊀cnf
cnf β€œβŠ₯”       = βŠ₯cnf
cnf (P β€œβˆ§β€ Q) = cnf P ∧cnf cnf Q
cnf (P β€œβˆ¨β€ Q) = cnf P ∨cnf cnf Q
cnf (β€œΒ¬β€ P)   = Β¬cnf (cnf P)

cnf-sound
  : βˆ€ (P : Proposition Ξ“) (ρ : Fin Ξ“ β†’ Bool)
  β†’ ⟦ cnf P ⟧ ρ ≑ ⟦ P ⟧ ρ
cnf-sound (atom x) ρ = and-truer (or (ρ x) false) βˆ™ or-falser (ρ x)

cnf-sound β€œβŠ€β€ ρ = refl
cnf-sound β€œβŠ₯” ρ = refl

cnf-sound (P β€œβˆ§β€ Q) ρ =
  ⟦ cnf P ∧cnf cnf Q ⟧ ρ           β‰‘βŸ¨ ∧cnf-sound (cnf P) (cnf Q) ρ βŸ©β‰‘
  and (⟦ cnf P ⟧ ρ) (⟦ cnf Q ⟧ ρ)  β‰‘βŸ¨ apβ‚‚ and (cnf-sound P ρ) (cnf-sound Q ρ) βŸ©β‰‘
  and (⟦ P ⟧ ρ) (⟦ Q ⟧ ρ)          ∎
cnf-sound (P β€œβˆ¨β€ Q) ρ =
  ⟦ cnf P ∨cnf cnf Q ⟧ ρ          β‰‘βŸ¨ ∨cnf-sound (cnf P) (cnf Q) ρ βŸ©β‰‘
  or (⟦ cnf P ⟧ ρ) (⟦ cnf Q ⟧ ρ)  β‰‘βŸ¨ apβ‚‚ or (cnf-sound P ρ) (cnf-sound Q ρ) βŸ©β‰‘
  or (⟦ P ⟧ ρ) (⟦ Q ⟧ ρ)          ∎
cnf-sound (β€œΒ¬β€ P) ρ =
  ⟦ Β¬cnf (cnf P) ⟧ ρ  β‰‘βŸ¨ Β¬cnf-sound (cnf P) ρ βŸ©β‰‘
  not (⟦ cnf P ⟧ ρ)   β‰‘βŸ¨ ap not (cnf-sound P ρ) βŸ©β‰‘
  not (⟦ P ⟧ ρ)       ∎

QuotationπŸ”—

We can also read expressions in CNF back into propositions. Luckily, there are no exponential blow-ups here!

quote-lit : Literal Ξ“ β†’ Proposition Ξ“
quote-lit (lit x) = atom x
quote-lit (neg x) = β€œΒ¬β€ (atom x)

quote-clause : Clause Ξ“ β†’ Proposition Ξ“
quote-clause []      = β€œβŠ₯”
quote-clause (x ∷ Ο•) = quote-lit x β€œβˆ¨β€ quote-clause Ο•

quote-cnf : CNF Ξ“ β†’ Proposition Ξ“
quote-cnf []       = β€œβŠ€β€
quote-cnf (Ο• ∷ Ο•s) = quote-clause Ο• β€œβˆ§β€ quote-cnf Ο•s

quote-lit-sound : βˆ€ (x : Literal Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ x ⟧ ρ ≑ ⟦ quote-lit x ⟧ ρ
quote-lit-sound (lit x) ρ = refl
quote-lit-sound (neg x) ρ = refl

quote-clause-sound : βˆ€ (Ο• : Clause Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ Ο• ⟧ ρ ≑ ⟦ quote-clause Ο• ⟧ ρ
quote-clause-sound []      ρ = refl
quote-clause-sound (x ∷ Ο•) ρ = apβ‚‚ or (quote-lit-sound x ρ) (quote-clause-sound Ο• ρ)

quote-cnf-sound : βˆ€ (Ο• : CNF Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ Ο• ⟧ ρ ≑ ⟦ quote-cnf Ο• ⟧ ρ
quote-cnf-sound []       ρ = refl
quote-cnf-sound (Ο• ∷ Ο•s) ρ = apβ‚‚ and (quote-clause-sound Ο• ρ) (quote-cnf-sound Ο•s ρ)

literal-eq-negate : βˆ€ (x y : Literal Ξ“) β†’ Β¬ x ≑ y β†’ lit-var x ≑ lit-var y β†’ x ≑ Β¬lit y
literal-eq-negate (lit x) (lit y) x≠y p = absurd (x≠y (ap lit p))
literal-eq-negate (lit x) (neg y) x≠y p = ap lit p
literal-eq-negate (neg x) (lit y) x≠y p = ap neg p
literal-eq-negate (neg x) (neg y) x≠y p = absurd (x≠y (ap neg p))

literal-sat-val : βˆ€ (x : Literal Ξ“) β†’ (ρ : Fin Ξ“ β†’ Bool) β†’ ⟦ x ⟧ ρ ≑ true β†’ ρ (lit-var x) ≑ lit-val x
literal-sat-val (lit x) ρ x-true = x-true
literal-sat-val (neg x) ρ x-true = not-inj x-true