parityOf_cons
The lemma establishes that parityOf on a cons list equals the XOR of the head variable's assigned value and the parity of the tail list. Researchers encoding or solving XOR-SAT instances would cite it for the inductive decomposition of parity constraints. The short tactic proof unfolds the foldl definition of parityOf, simplifies the cons case, invokes the foldl initialization helper, and reduces via Boolean XOR identities.
claimLet $a$ be an assignment of Boolean values to $n$ variables, let $v$ be a variable, and let $vs$ be a list of variables. Then the parity of $a$ over the list $v :: vs$ equals $a(v) ⊕$ (parity of $a$ over $vs$), where parity is the iterated Boolean XOR starting from false.
background
An assignment maps each variable (Fin n) to a Boolean value. The parityOf function on a list of variables is defined by folding XOR over the assigned values, beginning from false. This supplies the recursive case for parity computations on nonempty lists in the module defining XOR constraints, where each constraint requires the parity of a variable subset to equal a target parity value. The lemma depends on the helper foldl_xor_init, which equates a foldl starting from an arbitrary initial Boolean to the same foldl started from false, together with the definition of parityOf itself.
proof idea
Unfold the definition of parityOf to expose the foldl. Apply simp to handle the List.foldl_cons case. Rewrite with the foldl_xor_init lemma to normalize the initial value to false. Finish with rw on Bool.false_xor and Bool.xor_comm to obtain the head-XOR-tail form.
why it matters in Recognition Science
The result is invoked directly by xor_recover_value to extract a variable value from a list parity and by the backpropagation lemmas knownParity_eq_parityOf_known' and parityOf_filter_split' for handling partial assignments and filtered lists. It supplies the inductive step required for parity-based reasoning inside XOR-SAT encodings. Within the Recognition framework this supports the complexity layer that encodes satisfiability questions over parity constraints.
scope and limits
- Does not prove satisfiability or unsatisfiability of any XOR system.
- Does not cover the empty-list base case, which is handled by parityOf_nil.
- Does not address the semantics or satisfaction predicate of XOR constraints.
- Does not supply complexity bounds or reduction results.
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 -/