xor_recover_value
plain-language theorem explainer
The lemma recovers a variable's Boolean value as the XOR difference between the parity of a list containing it and the parity of its tail. Researchers encoding parity constraints in SAT solvers or complexity reductions would cite it when decomposing XOR systems into individual literals. The proof is a short tactic sequence that rewrites the cons case of parityOf, substitutes the tail parity, and applies a Boolean XOR cancellation calculation.
Claim. Let $a$ be a Boolean assignment to $n$ variables, $v$ a variable index, and $vs$ a list of variable indices. If the parity of $a$ on the list $v :: vs$ equals $p$ and the parity on $vs$ equals $q$, then $a(v) = poplus q$.
background
In the XOR module an assignment is a total function from variables (Fin n) to Bool. The parityOf operation folds Boolean XOR over the assignment values on a given list of variables, initialized at false. The supporting lemma parityOf_cons states that parityOf a (v :: vs) equals Bool.xor (a v) (parityOf a vs). The module treats XOR constraints as semantic parity conditions on subsets of variables, kept separate from CNF clauses rather than rewritten into them.
proof idea
The tactic rewrites hypothesis hp with parityOf_cons to obtain (a v) XOR (parityOf a vs) = p. It substitutes the tail parity q from hq, then applies a calc block: a v equals Bool.xor (Bool.xor (a v) (parityOf a vs)) (parityOf a vs) by simp, which reduces to Bool.xor p (parityOf a vs) by rw [hp] and finally to p XOR q.
why it matters
The lemma supplies the basic recovery step needed to extract literal values from parity constraints inside the SAT.XOR encoding. It sits inside the Complexity domain and supports the definition of SatisfiableXOR and related satisfiability predicates. No downstream uses are recorded yet; it closes a local algebraic identity rather than a framework-level forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.