Normal Forms — Core Definitions

This module defines Conjunctive Normal Form (CNF) and Disjunctive Normal Form (DNF) Boolean formulas over N variables, together with their evaluation semantics, complexity measures, and De Morgan negation duality.

Main definitions

• Literal — a Boolean variable with a polarity flag (positive or negative)
• CNF — a conjunction of clauses (each clause is a disjunction of literals)
• DNF — a disjunction of terms (each term is a conjunction of literals)
• CNF.complexity — the number of clauses in a CNF formula
• DNF.complexity — the number of terms in a DNF formula
• CNF.neg / DNF.neg — De Morgan negation (CNF ↔ DNF)

Relation to Complexity.SAT

Complexity.Literal, Complexity.CNF, and Complexity.DNF are deliberately distinct from Complexity.SAT.Lit and Complexity.SAT.CNF. The types here are Fin-indexed over a fixed variable count N and are used for circuit lower bounds, whereas the SAT versions are Nat-indexed and serve as the language encoding for SAT.

structure Complexity.Literal (N : ℕ) : Type

A literal: a Boolean variable (by index) together with a polarity flag.

polarity = true represents the positive literal xᵢ; polarity = false represents the negative literal ¬xᵢ.

• var : Fin N

  The index of the Boolean variable this literal refers to.

• polarity : Bool

  true = positive literal (xᵢ); false = negative literal (¬xᵢ).

@[implicit_reducible]

instance Complexity.instDecidableEqLiteral {N✝ : ℕ} : DecidableEq (Literal N✝)

Equations

• Complexity.instDecidableEqLiteral = Complexity.instDecidableEqLiteral.decEq

def Complexity.instDecidableEqLiteral.decEq {N✝ : ℕ} (x✝ x✝¹ : Literal N✝) : Decidable (x✝ = x✝¹)

Equations

• Complexity.instDecidableEqLiteral.decEq { var := a, polarity := a_1 } { var := b, polarity := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Complexity.Literal.eval {N : ℕ} (l : Literal N) (x : BitString N) : Bool

Evaluate a literal on a bit assignment.

Equations

• l.eval x = if l.polarity = true then x l.var else !x l.var

def Complexity.Literal.neg {N : ℕ} (l : Literal N) : Literal N

Negate a literal by flipping its polarity.

Equations

• l.neg = { var := l.var, polarity := !l.polarity }

theorem Complexity.Literal.eval_neg {N : ℕ} (l : Literal N) (x : BitString N) : l.neg.eval x = !l.eval x

Negating a literal negates its evaluation.

CNF

structure Complexity.CNF (N : ℕ) : Type

A CNF (Conjunctive Normal Form) formula over N Boolean variables.

A CNF is a conjunction of clauses, where each clause is a disjunction of literals.

• clauses : List (List (Literal N))

  The clauses of the formula. Each clause is a list of literals.

def Complexity.CNF.eval {N : ℕ} (φ : CNF N) (x : BitString N) : Bool

A CNF formula evaluates to true iff every clause contains at least one satisfied literal.

Equations

• φ.eval x = φ.clauses.all fun (clause : List (Complexity.Literal N)) => clause.any fun (l : Complexity.Literal N) => l.eval x

def Complexity.CNF.complexity {N : ℕ} (φ : CNF N) : ℕ

The complexity of a CNF formula is its number of clauses.

Equations

• φ.complexity = φ.clauses.length

DNF

structure Complexity.DNF (N : ℕ) : Type

A DNF (Disjunctive Normal Form) formula over N Boolean variables.

A DNF is a disjunction of terms, where each term is a conjunction of literals.

• terms : List (List (Literal N))

  The terms of the formula. Each term is a list of literals.

def Complexity.DNF.eval {N : ℕ} (φ : DNF N) (x : BitString N) : Bool

A DNF formula evaluates to true iff at least one term has all its literals satisfied.

Equations

• φ.eval x = φ.terms.any fun (term : List (Complexity.Literal N)) => term.all fun (l : Complexity.Literal N) => l.eval x

def Complexity.DNF.complexity {N : ℕ} (φ : DNF N) : ℕ

The complexity of a DNF formula is its number of terms.

Equations

• φ.complexity = φ.terms.length

De Morgan Negation Duality

def Complexity.CNF.neg {N : ℕ} (φ : CNF N) : DNF N

Negate a CNF formula by flipping all literal polarities, producing a DNF. By De Morgan's laws, ¬(∧ᵢ ∨ⱼ lᵢⱼ) = ∨ᵢ ∧ⱼ ¬lᵢⱼ.

Equations

• φ.neg = { terms := List.map (fun (clause : List (Complexity.Literal N)) => List.map Complexity.Literal.neg clause) φ.clauses }

def Complexity.DNF.neg {N : ℕ} (φ : DNF N) : CNF N

Negate a DNF formula by flipping all literal polarities, producing a CNF. By De Morgan's laws, ¬(∨ᵢ ∧ⱼ lᵢⱼ) = ∧ᵢ ∨ⱼ ¬lᵢⱼ.

Equations

• φ.neg = { clauses := List.map (fun (term : List (Complexity.Literal N)) => List.map Complexity.Literal.neg term) φ.terms }

theorem Complexity.CNF.eval_neg {N : ℕ} (φ : CNF N) (x : BitString N) : φ.neg.eval x = !φ.eval x

Negating a CNF formula negates its evaluation (De Morgan duality).

theorem Complexity.DNF.eval_neg {N : ℕ} (φ : DNF N) (x : BitString N) : φ.neg.eval x = !φ.eval x

Negating a DNF formula negates its evaluation (De Morgan duality).

theorem Complexity.CNF.complexity_neg {N : ℕ} (φ : CNF N) : φ.neg.complexity = φ.complexity

Negating a CNF preserves complexity.