Directed implication chains

Each link uses one binary clause. The logical direction of a subdivided wire is chosen so that truth of a literal at its clause endpoint implies truth of the source literal. Completeness only needs the constant assignment along a wire; soundness only needs implication in this one direction. No return wire is needed.

Main definitions

• Cslib.Logic.PL.CNF.implicationChain: binary implications along consecutive listed variables.

Main results

• Cslib.Logic.PL.CNF.eval_implicationChain: the individual link implications.
• Cslib.Logic.PL.CNF.true_getLastD_of_eval_implicationChain: truth propagates along a chain.
• Cslib.Logic.PL.CNF.eval_implicationChain_of_constant: constant signals satisfy all links.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3

def Cslib.Logic.PL.CNF.implicationChain {V : Type u_1} (vs : List V) : CNF V

One binary implication per consecutive pair; empty and singleton chains have no clauses.

theorem Cslib.Logic.PL.CNF.eval_implicationChain {V : Type u_1} (σ : V → Bool) (vs : List V) : eval σ (implicationChain vs) = true ↔ ∀ (p : V × V), p ∈ vs.consecutivePairs → σ p.fst = true → σ p.snd = true

A chain holds exactly when truth propagates across every consecutive link.

theorem Cslib.Logic.PL.CNF.true_getLastD_of_eval_implicationChain {V : Type u_1} (σ : V → Bool) (first : V) (rest : List V) (h : eval σ (implicationChain (first :: rest)) = true) (hf : σ first = true) : σ ((first :: rest).getLastD first) = true

A true signal at the first variable propagates to the last variable.

theorem Cslib.Logic.PL.CNF.eval_implicationChain_of_constant {V : Type u_1} (σ : V → Bool) (vs : List V) (value : Bool) (h : ∀ (v : V), v ∈ vs → σ v = value) : eval σ (implicationChain vs) = true

Assigning one value to every variable on the chain satisfies all of its implications.