parityOf_cons
The lemma states that the parity of an assignment over a cons list of variables equals the XOR of the head variable's value under the assignment and the parity over the tail list. Researchers encoding or solving XOR-SAT instances would cite it for inductive parity calculations on variable lists. The proof is a short term-mode reduction that unfolds the fold definition of parityOf, applies the foldl_xor_init helper, and simplifies via Boolean XOR identities.
claimLet $a$ be a Boolean assignment to $n$ variables, let $v$ be a variable index, and let $vs$ be a list of variable indices. Then the parity of $a$ on the list $v :: vs$ equals $a(v) ⊕$ the parity of $a$ on $vs$.
background
In the XOR module an assignment is a total function from Var n (abbreviated as Fin n) to Bool. The function parityOf a S is defined by folding left with XOR, starting from false, over the values a assigns to the variables in list S. This supports XOR constraints that require the parity of a variable subset to match a target Boolean value, complementing the CNF clause machinery imported from the CNF module.
proof idea
The proof unfolds parityOf to expose the foldl, simplifies the cons case of foldl, rewrites with the foldl_xor_init lemma to adjust the initial accumulator, and finishes with the Boolean identities false_xor and xor_comm.
why it matters in Recognition Science
The lemma supplies the recursive step for parity computations and is invoked directly in xor_recover_value to extract individual variable values from parity equations, as well as in the Backprop module lemmas knownParity_eq_parityOf_known' and parityOf_filter_split' for handling partial assignments. It forms part of the infrastructure for mixing XOR constraints with CNF in SAT encodings.
scope and limits
- Does not apply to the empty list case.
- Does not address satisfiability of XOR systems.
- Does not generalize beyond Boolean XOR.
- Does not prove uniqueness or existence of assignments.
Lean usage
rw [parityOf_cons] at hpformal statement (Lean)
72lemma parityOf_cons {n} (a : Assignment n) (v : Var n) (vs : List (Var n)) :
73 parityOf a (v :: vs) = Bool.xor (a v) (parityOf a vs) := by
proof body
Term-mode proof.
74 unfold parityOf
75 simp only [List.foldl_cons]
76 rw [foldl_xor_init]
77 rw [Bool.false_xor, Bool.xor_comm]
78
79/-- If parityOf a (v :: vs) = p and parityOf a vs = q, then a v = p ⊕ q -/