Evaluating a formula restricted by a partial assignment

The restriction φ.restrictBy ρ of a CNF formula by a partial assignment ρ (Cslib.Logic.PL.CNF.restrictBy) drops the clauses that ρ satisfies and removes the literals of the variables that ρ fixes from the others. This file relates it to φ under the total assignments that extend ρ.

Main results

• Cslib.Logic.PL.CNF.eval_restrictBy: under an assignment that extends ρ, the restricted formula has the value of φ.
• Cslib.Logic.PL.CNF.length_le_of_mem_restrictBy: restriction does not widen clauses.
• Cslib.Logic.PL.CNF.exists_preimage_restrictBy: a list of clauses of the restricted formula comes, clause by clause, from a list of clauses of φ with the same value under every extension of ρ.

theorem Cslib.Logic.PL.Clause.eval_filter_of_extends {V : Type u_1} {ρ : V → Option Bool} {γ : V → Bool} (hγ : ∀ (v : V) (b : Bool), ρ v = some b → γ v = b) {d : Clause V} (hd : ∀ l ∈ d, ρ l.1 ≠ some l.2) : eval γ (List.filter (fun (l : Literal V) => decide (ρ l.1 = none)) d) = eval γ d

Under an assignment that extends ρ, a clause that ρ does not satisfy has the value of its literals on the variables that ρ does not fix.

theorem Cslib.Logic.PL.CNF.eval_restrictBy {V : Type u_1} {φ : CNF V} {ρ : V → Option Bool} {γ : V → Bool} (hγ : ∀ (v : V) (b : Bool), ρ v = some b → γ v = b) : eval γ (φ.restrictBy ρ) = eval γ φ

Restriction preserves the value under extensions: an assignment that extends ρ satisfies φ.restrictBy ρ exactly when it satisfies φ.

theorem Cslib.Logic.PL.CNF.length_le_of_mem_restrictBy {V : Type u_1} {φ : CNF V} {ρ : V → Option Bool} {k : ℕ} (hlen : ∀ c ∈ φ, List.length c ≤ k) (c : Clause V) : c ∈ φ.restrictBy ρ → List.length c ≤ k

Restriction does not widen clauses.

theorem Cslib.Logic.PL.CNF.exists_preimage_restrictBy {V : Type u_1} {φ : CNF V} {ρ : V → Option Bool} {ψ : CNF V} : (∀ c ∈ ψ, c ∈ φ.restrictBy ρ) → ∃ (χ : CNF V), (∀ d ∈ χ, d ∈ φ) ∧ List.length χ = List.length ψ ∧ ∀ (γ : V → Bool), (∀ (v : V) (b : Bool), ρ v = some b → γ v = b) → eval γ χ = eval γ ψ

Preimages of restricted clauses: a list of clauses of φ.restrictBy ρ has, clause by clause, a list of clauses of φ of the same length with the same value under every extension of ρ.