Literals and bounded-width normal forms

This module supplies the finite syntax used by switching arguments. A literal stores the value that makes it true. A LiteralSet stores at most one literal per variable by using a partial assignment, so contradictory terms and tautological clauses are excluded by construction. Ordered lists of such sets form DNF and CNF formulas; the order will later make the canonical decision tree deterministic.

Restriction keeps the original variable names. A term falsified by a fixed literal is dropped from a DNF, while a clause satisfied by a fixed literal is dropped from a CNF. Empty terms and clauses represent the Boolean constants true and false respectively.

structure Algebraic.AC0.Literal (n : ℕ) : Type

A signed Boolean variable, represented by the value that makes the literal true. Thus value = true is a positive literal and value = false is a negative literal.

• index : Fin n

  The input coordinate read by the literal.

• value : Bool

  The Boolean value that satisfies the literal.

@[instance_reducible]

instance Algebraic.AC0.instDecidableEqLiteral {n✝ : ℕ} : DecidableEq (Literal n✝)

Equations

• Algebraic.AC0.instDecidableEqLiteral = Algebraic.AC0.instDecidableEqLiteral.decEq

def Algebraic.AC0.instDecidableEqLiteral.decEq {n✝ : ℕ} (x✝ x✝¹ : Literal n✝) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.AC0.instDecidableEqLiteral.decEq { index := a, value := a_1 } { index := b, value := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Algebraic.AC0.Literal.eval {n : ℕ} (literal : Literal n) (input : Fin n → Bool) : Bool

Evaluate a literal on a complete Boolean input.

Equations

• literal.eval input = decide (input literal.index = literal.value)

@[simp]

theorem Algebraic.AC0.Literal.eval_eq_true {n : ℕ} (literal : Literal n) (input : Fin n → Bool) : literal.eval input = true ↔ input literal.index = literal.value

def Algebraic.AC0.Literal.negate {n : ℕ} (literal : Literal n) : Literal n

Boolean negation of a literal.

Equations

• literal.negate = { index := literal.index, value := !literal.value }

@[simp]

theorem Algebraic.AC0.Literal.negate_index {n : ℕ} (literal : Literal n) : literal.negate.index = literal.index

@[simp]

theorem Algebraic.AC0.Literal.negate_value {n : ℕ} (literal : Literal n) : literal.negate.value = !literal.value

@[simp]

theorem Algebraic.AC0.Literal.negate_negate {n : ℕ} (literal : Literal n) : literal.negate.negate = literal

@[simp]

theorem Algebraic.AC0.Literal.eval_negate {n : ℕ} (literal : Literal n) (input : Fin n → Bool) : literal.negate.eval input = !literal.eval input

structure Algebraic.AC0.LiteralSet (n : ℕ) : Type

A finite, noncontradictory collection of literals. The partial assignment records the truth value required of each variable that occurs.

• requirements : PartialAssignment n

  Partial map from occurring variables to their satisfying values.

@[instance_reducible]

instance Algebraic.AC0.instDecidableEqLiteralSet {n✝ : ℕ} : DecidableEq (LiteralSet n✝)

Equations

• Algebraic.AC0.instDecidableEqLiteralSet = Algebraic.AC0.instDecidableEqLiteralSet.decEq

def Algebraic.AC0.instDecidableEqLiteralSet.decEq {n✝ : ℕ} (x✝ x✝¹ : LiteralSet n✝) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.AC0.instDecidableEqLiteralSet.decEq { requirements := a } { requirements := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Algebraic.AC0.LiteralSet.empty {n : ℕ} : LiteralSet n

The empty collection of literals.

Equations

• Algebraic.AC0.LiteralSet.empty = { requirements := Algebraic.PartialAssignment.empty }

def Algebraic.AC0.LiteralSet.singleton {n : ℕ} (literal : Literal n) : LiteralSet n

The one-element collection containing a literal.

Equations

• Algebraic.AC0.LiteralSet.singleton literal = { requirements := Algebraic.PartialAssignment.fix literal.index literal.value }

def Algebraic.AC0.LiteralSet.support {n : ℕ} (set : LiteralSet n) : Finset (Fin n)

Variables occurring in a literal collection.

Equations

• set.support = set.requirements.fixedVariables

@[simp]

theorem Algebraic.AC0.LiteralSet.mem_support {n : ℕ} (set : LiteralSet n) (index : Fin n) : index ∈ set.support ↔ set.requirements index ≠ none

def Algebraic.AC0.LiteralSet.width {n : ℕ} (set : LiteralSet n) : ℕ

Width of a literal collection.

Equations

• set.width = set.support.card

@[simp]

theorem Algebraic.AC0.LiteralSet.support_empty {n : ℕ} : empty.support = ∅

@[simp]

theorem Algebraic.AC0.LiteralSet.width_empty {n : ℕ} : empty.width = 0

def Algebraic.AC0.LiteralSet.residual {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : LiteralSet n

Remove the literals whose variables have been fixed by rho. This operation does not itself check whether those fixed values satisfy or falsify the removed literals.

Equations

• set.residual rho = { requirements := fun (index : Fin n) => match rho index with | none => set.requirements index | some val => none }

@[simp]

theorem Algebraic.AC0.LiteralSet.residual_requirements_of_live {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) {index : Fin n} (live : rho index = none) : (set.residual rho).requirements index = set.requirements index

@[simp]

theorem Algebraic.AC0.LiteralSet.residual_requirements_of_fixed {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) {index : Fin n} {value : Bool} (fixed : rho index = some value) : (set.residual rho).requirements index = none

theorem Algebraic.AC0.LiteralSet.support_residual_subset {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : (set.residual rho).support ⊆ set.support

Restriction only removes variables from a literal collection.

theorem Algebraic.AC0.LiteralSet.support_residual_subset_live {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : (set.residual rho).support ⊆ rho.liveVariables

Every literal remaining after restriction is on a variable left live by the restriction.

theorem Algebraic.AC0.LiteralSet.width_residual_le {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : (set.residual rho).width ≤ set.width

Restriction cannot increase the width of a literal collection.

def Algebraic.AC0.LiteralSet.ConflictsWith {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : Prop

Some fixed literal of set is falsified by rho.

Equations

• set.ConflictsWith rho = ∃ (index : Fin n) (required : Bool) (fixed : Bool), set.requirements index = some required ∧ rho index = some fixed ∧ required ≠ fixed

@[instance_reducible]

instance Algebraic.AC0.LiteralSet.conflictsWithDecidable {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : Decidable (set.ConflictsWith rho)

Equations

• set.conflictsWithDecidable rho = id inferInstance

theorem Algebraic.AC0.LiteralSet.ConflictsWith.refine {n : ℕ} {set : LiteralSet n} {rho : PartialAssignment n} (conflict : set.ConflictsWith rho) (extension : PartialAssignment n) : set.ConflictsWith (rho.refine extension)

A conflict witnessed by an existing fixed variable persists under every later refinement.

def Algebraic.AC0.LiteralSet.HitBy {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : Prop

Some fixed literal of set is satisfied by rho.

Equations

• set.HitBy rho = ∃ (index : Fin n) (value : Bool), set.requirements index = some value ∧ rho index = some value

@[instance_reducible]

instance Algebraic.AC0.LiteralSet.hitByDecidable {n : ℕ} (set : LiteralSet n) (rho : PartialAssignment n) : Decidable (set.HitBy rho)

Equations

• set.hitByDecidable rho = id inferInstance

@[reducible, inline]

abbrev Algebraic.AC0.Term (n : ℕ) : Type

A conjunction of distinct-variable literals.

Equations

• Algebraic.AC0.Term n = Algebraic.AC0.LiteralSet n

def Algebraic.AC0.Term.SatisfiedBy {n : ℕ} (term : Term n) (input : Fin n → Bool) : Prop

A complete input satisfies a term when it gives every occurring literal its required value.

Equations

• term.SatisfiedBy input = ∀ (index : Fin n) (value : Bool), term.requirements index = some value → input index = value

@[instance_reducible]

instance Algebraic.AC0.Term.satisfiedByDecidable {n : ℕ} (term : Term n) (input : Fin n → Bool) : Decidable (term.SatisfiedBy input)

Equations

• term.satisfiedByDecidable input = id inferInstance

def Algebraic.AC0.Term.eval {n : ℕ} (term : Term n) (input : Fin n → Bool) : Bool

Boolean semantics of a term. The empty term is true.

Equations

• term.eval input = decide (term.SatisfiedBy input)

@[simp]

theorem Algebraic.AC0.Term.eval_eq_true {n : ℕ} (term : Term n) (input : Fin n → Bool) : term.eval input = true ↔ term.SatisfiedBy input

@[simp]

theorem Algebraic.AC0.Term.eval_empty {n : ℕ} (input : Fin n → Bool) : eval LiteralSet.empty input = true

def Algebraic.AC0.Term.restrict {n : ℕ} (term : Term n) (rho : PartialAssignment n) : Option (Term n)

Restrict a term. none denotes a term made constantly false by a conflicting fixed literal; otherwise the remaining live literals are returned.

Equations

• term.restrict rho = if Algebraic.AC0.LiteralSet.ConflictsWith term rho then none else some (Algebraic.AC0.LiteralSet.residual term rho)

theorem Algebraic.AC0.Term.eval_apply_eq_false_of_conflicts {n : ℕ} (term : Term n) (rho : PartialAssignment n) (input : Fin n → Bool) (conflict : LiteralSet.ConflictsWith term rho) : term.eval (rho.apply input) = false

A conflicting partial assignment makes a term false under every completion.

theorem Algebraic.AC0.Term.eval_residual_eq_eval_apply_of_not_conflicts {n : ℕ} (term : Term n) (rho : PartialAssignment n) (input : Fin n → Bool) (noConflict : ¬LiteralSet.ConflictsWith term rho) : eval (LiteralSet.residual term rho) input = term.eval (rho.apply input)

In the absence of a conflict, evaluating the residual term is exactly evaluation of the original term under the partial assignment.

theorem Algebraic.AC0.Term.restrict_sound {n : ℕ} (term : Term n) (rho : PartialAssignment n) (input : Fin n → Bool) : ((term.restrict rho).elim false fun (residual : Term n) => residual.eval input) = term.eval (rho.apply input)

Total semantic specification of term restriction.

theorem Algebraic.AC0.Term.width_restrict_le {n : ℕ} (term residual : Term n) (rho : PartialAssignment n) (restricted : term.restrict rho = some residual) : LiteralSet.width residual ≤ LiteralSet.width term

Any residual returned by term restriction has no greater width than the source term.

@[reducible, inline]

abbrev Algebraic.AC0.Clause (n : ℕ) : Type

A disjunction of distinct-variable literals.

Equations

• Algebraic.AC0.Clause n = Algebraic.AC0.LiteralSet n

def Algebraic.AC0.Clause.SatisfiedBy {n : ℕ} (clause : Clause n) (input : Fin n → Bool) : Prop

A complete input satisfies a clause when it satisfies at least one occurring literal.

Equations

• clause.SatisfiedBy input = ∃ (index : Fin n) (value : Bool), clause.requirements index = some value ∧ input index = value

@[instance_reducible]

instance Algebraic.AC0.Clause.satisfiedByDecidable {n : ℕ} (clause : Clause n) (input : Fin n → Bool) : Decidable (clause.SatisfiedBy input)

Equations

• clause.satisfiedByDecidable input = id inferInstance

def Algebraic.AC0.Clause.eval {n : ℕ} (clause : Clause n) (input : Fin n → Bool) : Bool

Boolean semantics of a clause. The empty clause is false.

Equations

• clause.eval input = decide (clause.SatisfiedBy input)

@[simp]

theorem Algebraic.AC0.Clause.eval_eq_true {n : ℕ} (clause : Clause n) (input : Fin n → Bool) : clause.eval input = true ↔ clause.SatisfiedBy input

@[simp]

theorem Algebraic.AC0.Clause.eval_empty {n : ℕ} (input : Fin n → Bool) : eval LiteralSet.empty input = false

def Algebraic.AC0.Clause.restrict {n : ℕ} (clause : Clause n) (rho : PartialAssignment n) : Option (Clause n)

Restrict a clause. none denotes a clause made constantly true by a satisfied fixed literal; otherwise the remaining live literals are returned.

Equations

• clause.restrict rho = if Algebraic.AC0.LiteralSet.HitBy clause rho then none else some (Algebraic.AC0.LiteralSet.residual clause rho)

theorem Algebraic.AC0.Clause.eval_apply_eq_true_of_hit {n : ℕ} (clause : Clause n) (rho : PartialAssignment n) (input : Fin n → Bool) (hit : LiteralSet.HitBy clause rho) : clause.eval (rho.apply input) = true

A fixed literal satisfying a clause makes it true under every completion.

theorem Algebraic.AC0.Clause.eval_residual_eq_eval_apply_of_not_hit {n : ℕ} (clause : Clause n) (rho : PartialAssignment n) (input : Fin n → Bool) (noHit : ¬LiteralSet.HitBy clause rho) : eval (LiteralSet.residual clause rho) input = clause.eval (rho.apply input)

If no fixed literal satisfies a clause, evaluating the residual clause is exactly evaluation of the original clause under the partial assignment.

theorem Algebraic.AC0.Clause.restrict_sound {n : ℕ} (clause : Clause n) (rho : PartialAssignment n) (input : Fin n → Bool) : ((clause.restrict rho).elim true fun (residual : Clause n) => residual.eval input) = clause.eval (rho.apply input)

Total semantic specification of clause restriction.

theorem Algebraic.AC0.Clause.width_restrict_le {n : ℕ} (clause residual : Clause n) (rho : PartialAssignment n) (restricted : clause.restrict rho = some residual) : LiteralSet.width residual ≤ LiteralSet.width clause

Any residual returned by clause restriction has no greater width than the source clause.

structure Algebraic.AC0.DNF (n : ℕ) : Type

An ordered disjunction of terms. Ordering is semantically irrelevant but is retained for the canonical decision-tree construction.

• terms : List (Term n)

  Terms in the deterministic order used by canonical constructions.

@[instance_reducible]

instance Algebraic.AC0.instDecidableEqDNF {n✝ : ℕ} : DecidableEq (DNF n✝)

Equations

• Algebraic.AC0.instDecidableEqDNF = Algebraic.AC0.instDecidableEqDNF.decEq

def Algebraic.AC0.instDecidableEqDNF.decEq {n✝ : ℕ} (x✝ x✝¹ : DNF n✝) : Decidable (x✝ = x✝¹)

Equations

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

def Algebraic.AC0.DNF.eval {n : ℕ} (formula : DNF n) (input : Fin n → Bool) : Bool

Boolean semantics of a DNF. The empty list is false.

Equations

• formula.eval input = formula.terms.any fun (term : Algebraic.AC0.Term n) => term.eval input

@[simp]

theorem Algebraic.AC0.DNF.eval_eq_true {n : ℕ} (formula : DNF n) (input : Fin n → Bool) : formula.eval input = true ↔ ∃ term ∈ formula.terms, term.SatisfiedBy input

def Algebraic.AC0.DNF.bottom {n : ℕ} : DNF n

The constantly false DNF.

Equations

• Algebraic.AC0.DNF.bottom = { terms := [] }

def Algebraic.AC0.DNF.top {n : ℕ} : DNF n

The constantly true DNF, represented by one empty term.

Equations

• Algebraic.AC0.DNF.top = { terms := [Algebraic.AC0.LiteralSet.empty] }

@[simp]

theorem Algebraic.AC0.DNF.eval_bottom {n : ℕ} (input : Fin n → Bool) : bottom.eval input = false

@[simp]

theorem Algebraic.AC0.DNF.eval_top {n : ℕ} (input : Fin n → Bool) : top.eval input = true

def Algebraic.AC0.DNF.WidthAtMost {n : ℕ} (formula : DNF n) (bound : ℕ) : Prop

Every term in the DNF has width at most bound.

Equations

• formula.WidthAtMost bound = ∀ term ∈ formula.terms, Algebraic.AC0.LiteralSet.width term ≤ bound

def Algebraic.AC0.DNF.restrict {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) : DNF n

Restrict each term and discard those made constantly false.

Equations

• formula.restrict rho = { terms := List.filterMap (fun (term : Algebraic.AC0.Term n) => term.restrict rho) formula.terms }

theorem Algebraic.AC0.DNF.restrict_sound {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) (input : Fin n → Bool) : (formula.restrict rho).eval input = formula.eval (rho.apply input)

Restricting a DNF preserves its Boolean function exactly.

theorem Algebraic.AC0.DNF.widthAtMost_restrict {n : ℕ} (formula : DNF n) (rho : PartialAssignment n) {bound : ℕ} (bounded : formula.WidthAtMost bound) : (formula.restrict rho).WidthAtMost bound

Restriction preserves an upper bound on DNF term width.

theorem Algebraic.AC0.DNF.WidthAtMost.mono {n : ℕ} {formula : DNF n} {smaller larger : ℕ} (bounded : formula.WidthAtMost smaller) (le : smaller ≤ larger) : formula.WidthAtMost larger

A DNF width bound remains valid after increasing the allowance.

structure Algebraic.AC0.CNF (n : ℕ) : Type

An ordered conjunction of clauses. Ordering is retained so dual arguments can use the same canonical conventions as DNF.

• clauses : List (Clause n)

  Clauses in a retained deterministic order.

@[instance_reducible]

instance Algebraic.AC0.instDecidableEqCNF {n✝ : ℕ} : DecidableEq (CNF n✝)

Equations

• Algebraic.AC0.instDecidableEqCNF = Algebraic.AC0.instDecidableEqCNF.decEq

def Algebraic.AC0.instDecidableEqCNF.decEq {n✝ : ℕ} (x✝ x✝¹ : CNF n✝) : Decidable (x✝ = x✝¹)

Equations

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

def Algebraic.AC0.CNF.eval {n : ℕ} (formula : CNF n) (input : Fin n → Bool) : Bool

Boolean semantics of a CNF. The empty list is true.

Equations

• formula.eval input = formula.clauses.all fun (clause : Algebraic.AC0.Clause n) => clause.eval input

@[simp]

theorem Algebraic.AC0.CNF.eval_eq_true {n : ℕ} (formula : CNF n) (input : Fin n → Bool) : formula.eval input = true ↔ ∀ clause ∈ formula.clauses, clause.SatisfiedBy input

def Algebraic.AC0.CNF.top {n : ℕ} : CNF n

The constantly true CNF.

Equations

• Algebraic.AC0.CNF.top = { clauses := [] }

def Algebraic.AC0.CNF.bottom {n : ℕ} : CNF n

The constantly false CNF, represented by one empty clause.

Equations

• Algebraic.AC0.CNF.bottom = { clauses := [Algebraic.AC0.LiteralSet.empty] }

@[simp]

theorem Algebraic.AC0.CNF.eval_top {n : ℕ} (input : Fin n → Bool) : top.eval input = true

@[simp]

theorem Algebraic.AC0.CNF.eval_bottom {n : ℕ} (input : Fin n → Bool) : bottom.eval input = false

def Algebraic.AC0.CNF.WidthAtMost {n : ℕ} (formula : CNF n) (bound : ℕ) : Prop

Every clause in the CNF has width at most bound.

Equations

• formula.WidthAtMost bound = ∀ clause ∈ formula.clauses, Algebraic.AC0.LiteralSet.width clause ≤ bound

def Algebraic.AC0.CNF.restrict {n : ℕ} (formula : CNF n) (rho : PartialAssignment n) : CNF n

Restrict each clause and discard those made constantly true.

Equations

• formula.restrict rho = { clauses := List.filterMap (fun (clause : Algebraic.AC0.Clause n) => clause.restrict rho) formula.clauses }

theorem Algebraic.AC0.CNF.restrict_sound {n : ℕ} (formula : CNF n) (rho : PartialAssignment n) (input : Fin n → Bool) : (formula.restrict rho).eval input = formula.eval (rho.apply input)

Restricting a CNF preserves its Boolean function exactly.

theorem Algebraic.AC0.CNF.widthAtMost_restrict {n : ℕ} (formula : CNF n) (rho : PartialAssignment n) {bound : ℕ} (bounded : formula.WidthAtMost bound) : (formula.restrict rho).WidthAtMost bound

Restriction preserves an upper bound on CNF clause width.

theorem Algebraic.AC0.CNF.WidthAtMost.mono {n : ℕ} {formula : CNF n} {smaller larger : ℕ} (bounded : formula.WidthAtMost smaller) (le : smaller ≤ larger) : formula.WidthAtMost larger

A CNF width bound remains valid after increasing the allowance.