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.width / DNF.width — the largest clause/term length
• 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.instReprLiteral {N✝ : ℕ} : Repr (Literal N✝)

Equations

• Complexity.instReprLiteral = { reprPrec := Complexity.instReprLiteral.repr }

def Complexity.instReprLiteral.repr {N✝ : ℕ} : Literal N✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[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 }

@[simp]

theorem Complexity.Literal.neg_neg {N : ℕ} (literal : Literal N) : literal.neg.neg = literal

Literal negation is an involution.

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.

def Complexity.Literal.vars {N : ℕ} (literals : List (Literal N)) : Finset (Fin N)

The set of variables occurring in a list of literals.

Equations

• Complexity.Literal.vars literals = List.foldr (fun (literal : Complexity.Literal N) (support : Finset (Fin N)) => insert literal.var support) ∅ literals

@[simp]

theorem Complexity.Literal.vars_nil {N : ℕ} : vars [] = ∅

@[simp]

theorem Complexity.Literal.vars_cons {N : ℕ} (literal : Literal N) (literals : List (Literal N)) : vars (literal :: literals) = insert literal.var (vars literals)

theorem Complexity.Literal.mem_vars_iff {N : ℕ} (literals : List (Literal N)) (index : Fin N) : index ∈ vars literals ↔ ∃ literal ∈ literals, literal.var = index

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.

@[implicit_reducible]

instance Complexity.instReprCNF {N✝ : ℕ} : Repr (CNF N✝)

Equations

• Complexity.instReprCNF = { reprPrec := Complexity.instReprCNF.repr }

def Complexity.instReprCNF.repr {N✝ : ℕ} : CNF N✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.instDecidableEqCNF {N✝ : ℕ} : DecidableEq (CNF N✝)

Equations

• Complexity.instDecidableEqCNF = Complexity.instDecidableEqCNF.decEq

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

Equations

• Complexity.instDecidableEqCNF.decEq { clauses := a } { clauses := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

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

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

The width of a CNF is the maximum number of literals in any clause.

Equations

• φ.width = List.foldr (fun (clause : List (Complexity.Literal N)) (rest : ℕ) => max clause.length rest) 0 φ.clauses

theorem Complexity.CNF.length_le_width {N : ℕ} (φ : CNF N) (clause : List (Literal N)) (hclause : clause ∈ φ.clauses) : clause.length ≤ φ.width

Every clause length is bounded by the declared CNF width.

theorem Complexity.CNF.width_le_iff {N : ℕ} (φ : CNF N) (bound : ℕ) : φ.width ≤ bound ↔ ∀ clause ∈ φ.clauses, clause.length ≤ bound

A natural number bounds CNF width exactly when it bounds every clause length.

def Complexity.CNF.vars {N : ℕ} (φ : CNF N) : Finset (Fin N)

The set of variables occurring in a CNF.

Equations

• φ.vars = List.foldr (fun (clause : List (Complexity.Literal N)) (rest : Finset (Fin N)) => Complexity.Literal.vars clause ∪ rest) ∅ φ.clauses

@[simp]

theorem Complexity.CNF.vars_nil {N : ℕ} : { clauses := [] }.vars = ∅

@[simp]

theorem Complexity.CNF.vars_cons {N : ℕ} (clause : List (Literal N)) (clauses : List (List (Literal N))) : { clauses := clause :: clauses }.vars = Literal.vars clause ∪ { clauses := clauses }.vars

theorem Complexity.CNF.mem_vars_iff {N : ℕ} (φ : CNF N) (index : Fin N) : index ∈ φ.vars ↔ ∃ clause ∈ φ.clauses, ∃ literal ∈ clause, literal.var = index

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.

@[implicit_reducible]

instance Complexity.instReprDNF {N✝ : ℕ} : Repr (DNF N✝)

Equations

• Complexity.instReprDNF = { reprPrec := Complexity.instReprDNF.repr }

def Complexity.instReprDNF.repr {N✝ : ℕ} : DNF N✝ → ℕ → Std.Format

Equations

• Complexity.instReprDNF.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "terms" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.terms)).group) " }"

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

Equations

• Complexity.instDecidableEqDNF.decEq { terms := a } { terms := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.instDecidableEqDNF {N✝ : ℕ} : DecidableEq (DNF N✝)

Equations

• Complexity.instDecidableEqDNF = Complexity.instDecidableEqDNF.decEq

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

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

The width of a DNF is the maximum number of literals in any term.

Equations

• φ.width = List.foldr (fun (term : List (Complexity.Literal N)) (rest : ℕ) => max term.length rest) 0 φ.terms

theorem Complexity.DNF.length_le_width {N : ℕ} (φ : DNF N) (term : List (Literal N)) (hterm : term ∈ φ.terms) : term.length ≤ φ.width

Every term length is bounded by the declared DNF width.

theorem Complexity.DNF.width_le_iff {N : ℕ} (φ : DNF N) (bound : ℕ) : φ.width ≤ bound ↔ ∀ term ∈ φ.terms, term.length ≤ bound

A natural number bounds DNF width exactly when it bounds every term length.

def Complexity.DNF.vars {N : ℕ} (φ : DNF N) : Finset (Fin N)

The set of variables occurring in a DNF.

Equations

• φ.vars = List.foldr (fun (term : List (Complexity.Literal N)) (rest : Finset (Fin N)) => Complexity.Literal.vars term ∪ rest) ∅ φ.terms

@[simp]

theorem Complexity.DNF.vars_nil {N : ℕ} : { terms := [] }.vars = ∅

@[simp]

theorem Complexity.DNF.vars_cons {N : ℕ} (term : List (Literal N)) (terms : List (List (Literal N))) : { terms := term :: terms }.vars = Literal.vars term ∪ { terms := terms }.vars

theorem Complexity.DNF.mem_vars_iff {N : ℕ} (φ : DNF N) (index : Fin N) : index ∈ φ.vars ↔ ∃ term ∈ φ.terms, ∃ literal ∈ term, literal.var = index

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 }

@[simp]

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

De Morgan negation from CNF to DNF and back is an involution.

@[simp]

theorem Complexity.DNF.neg_neg {N : ℕ} (φ : DNF N) : φ.neg.neg = φ

De Morgan negation from DNF to CNF and back is an involution.

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.vars_neg {N : ℕ} (φ : CNF N) : φ.neg.vars = φ.vars

Negating a CNF preserves its variable support.

theorem Complexity.DNF.vars_neg {N : ℕ} (φ : DNF N) : φ.neg.vars = φ.vars

Negating a DNF preserves its variable support.

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

Negating a CNF preserves complexity.

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

Negating a DNF preserves complexity.

theorem Complexity.CNF.width_neg {N : ℕ} (φ : CNF N) : φ.neg.width = φ.width

Negating a CNF preserves width.

theorem Complexity.DNF.width_neg {N : ℕ} (φ : DNF N) : φ.neg.width = φ.width

Negating a DNF preserves width.