Total-function semantics for Tseitin splitting

The public SAT semantics use finite Boolean lists, with out-of-range variables defaulting to false. Fresh-variable arguments are simpler with total assignments ℕ → Bool, since a fresh variable can be set with Function.update without changing any earlier variable.

This internal module defines total-assignment evaluation for literals, clauses, and CNFs. It relates that evaluation to the existing list semantics, proves the two satisfiability notions equivalent, and records the congruence and update lemmas used by the recursive Tseitin correctness proof.

@[reducible, inline]

abbrev Complexity.SAT.TotalAssignment : Type

A total Boolean assignment, used internally while choosing fresh variables.

Equations

• Complexity.SAT.TotalAssignment = (ℕ → Bool)

@[inline]

def Complexity.SAT.Lit.evalTotal (α : TotalAssignment) (ℓ : Lit) : Bool

Evaluate a literal under a total assignment.

Equations

• Complexity.SAT.Lit.evalTotal α ℓ = (α ℓ.var == ℓ.sign)

@[simp]

theorem Complexity.SAT.Lit.evalTotal_get_internal (α : Assignment) (ℓ : Lit) : evalTotal α.get ℓ = eval α ℓ

Total evaluation through the Assignment.get view of a finite assignment agrees with the public list semantics.

@[simp]

theorem Complexity.SAT.Lit.evalTotal_neg_internal (α : TotalAssignment) (ℓ : Lit) : evalTotal α ℓ.neg = !evalTotal α ℓ

Negating a literal complements its value under a total assignment.

@[simp]

theorem Complexity.SAT.Lit.evalTotal_pos_internal (α : TotalAssignment) (v : ℕ) : evalTotal α (pos v) = α v

A positive literal evaluates to the value of its variable.

@[simp]

theorem Complexity.SAT.Lit.evalTotal_negVar_internal (α : TotalAssignment) (v : ℕ) : evalTotal α (negVar v) = !α v

A negative literal evaluates to the complement of its variable.

theorem Complexity.SAT.Lit.evalTotal_eq_of_agree_internal {α β : TotalAssignment} (ℓ : Lit) (h : α ℓ.var = β ℓ.var) : evalTotal α ℓ = evalTotal β ℓ

A literal has the same value under assignments that agree at its variable.

@[inline]

def Complexity.SAT.Clause.evalTotal (α : TotalAssignment) (c : Clause) : Bool

Evaluate a clause under a total assignment.

Equations

• Complexity.SAT.Clause.evalTotal α c = List.any c (Complexity.SAT.Lit.evalTotal α)

@[simp]

theorem Complexity.SAT.Clause.evalTotal_get_internal (α : Assignment) (c : Clause) : evalTotal α.get c = eval α c

Total evaluation through the Assignment.get view of a finite assignment agrees with the public list semantics.

theorem Complexity.SAT.Clause.evalTotal_eq_of_agree_internal {α β : TotalAssignment} (c : Clause) (h : ∀ ℓ ∈ c, α ℓ.var = β ℓ.var) : evalTotal α c = evalTotal β c

Clause evaluation is invariant when assignments agree on every occurring variable.

@[inline]

def Complexity.SAT.CNF.evalTotal (α : TotalAssignment) (φ : CNF) : Bool

Evaluate a CNF under a total assignment.

Equations

• Complexity.SAT.CNF.evalTotal α φ = List.all φ (Complexity.SAT.Clause.evalTotal α)

def Complexity.SAT.CNF.FunctionSatisfiable (φ : CNF) : Prop

A CNF is satisfiable by a total Boolean assignment.

Equations

• φ.FunctionSatisfiable = ∃ (α : Complexity.SAT.TotalAssignment), Complexity.SAT.CNF.evalTotal α φ = true

@[simp]

theorem Complexity.SAT.CNF.evalTotal_get_internal (α : Assignment) (φ : CNF) : evalTotal α.get φ = eval α φ

Total evaluation through the Assignment.get view of a finite assignment agrees with the public list semantics.

theorem Complexity.SAT.CNF.evalTotal_eq_of_agree_internal {α β : TotalAssignment} (φ : CNF) (h : ∀ c ∈ φ, ∀ ℓ ∈ c, α ℓ.var = β ℓ.var) : evalTotal α φ = evalTotal β φ

CNF evaluation is invariant when assignments agree on every occurring variable.

theorem Complexity.SAT.TotalAssignment.update_same_internal (α : TotalAssignment) (i : ℕ) (b : Bool) : Function.update α i b i = b

Updating a total assignment sets the selected variable to the new value.

theorem Complexity.SAT.TotalAssignment.update_of_ne_internal (α : TotalAssignment) {fresh i : ℕ} (b : Bool) (h : fresh ≠ i) : Function.update α fresh b i = α i

Updating one variable leaves every distinct variable unchanged.

theorem Complexity.SAT.TotalAssignment.update_of_lt_internal (α : TotalAssignment) (fresh i : ℕ) (b : Bool) (h : i < fresh) : Function.update α fresh b i = α i

Updating a total assignment at fresh leaves every smaller variable unchanged.

theorem Complexity.SAT.Lit.evalTotal_update_of_var_lt_internal (α : TotalAssignment) (fresh : ℕ) (b : Bool) (ℓ : Lit) (h : ℓ.var < fresh) : evalTotal (Function.update α fresh b) ℓ = evalTotal α ℓ

Updating a later variable preserves a literal's value.

theorem Complexity.SAT.Clause.evalTotal_update_of_maxVar_lt_internal (α : TotalAssignment) (fresh : ℕ) (b : Bool) (c : Clause) (h : c.maxVar < fresh) : evalTotal (Function.update α fresh b) c = evalTotal α c

Updating a variable above a clause's maximum variable preserves its value.

theorem Complexity.SAT.CNF.evalTotal_update_of_maxVar_lt_internal (α : TotalAssignment) (fresh : ℕ) (b : Bool) (φ : CNF) (h : φ.maxVar < fresh) : evalTotal (Function.update α fresh b) φ = evalTotal α φ

Updating a variable above a CNF's maximum variable preserves its value.

theorem Complexity.SAT.CNF.satisfiable_iff_functionSatisfiable_internal (φ : CNF) : φ.Satisfiable ↔ φ.FunctionSatisfiable

List satisfiability is equivalent to satisfiability by a total Boolean function.