foldl_xor_init
The identity for left-folding Boolean XOR states that the iterated XOR of variable values under an assignment, begun at an arbitrary initial Boolean, equals that initial value XORed with the identical fold begun at false. Researchers formalizing parity constraints or SAT encodings for Boolean satisfiability cite the result when rewriting XOR expressions. The proof proceeds by induction on the input list, applying the inductive hypothesis to two shifted initial values followed by associativity and false-XOR simplification.
claimLet $a$ be an assignment of Booleans to $n$ variables, let $b$ be an initial Boolean, and let $vs$ be a list of variable indices. Then the left fold $b$ XOR $a(v_1)$ XOR $...$ XOR $a(v_k)$ equals $b$ XOR (false XOR $a(v_1)$ XOR $...$ XOR $a(v_k)$).
background
An assignment for $n$ variables is a map from Fin $n$ to Bool; the parity of a subset is obtained by folding XOR over the list of values that the assignment returns for those variables. The module develops XOR constraints in which the parity of a chosen subset must equal a prescribed target parity. The relevant upstream definitions are the Assignment and Var abbreviations in the CNF module, which supply the types used here.
proof idea
The proof is by induction on the list $vs$, generalizing over the initial Boolean. The nil case is immediate by simplification. In the cons case the foldl_cons rule is applied, the inductive hypothesis is invoked once for each of the two shifted initials (init XOR a v and false XOR a v), false_xor is simplified, and associativity of XOR is used to equate the two sides.
why it matters in Recognition Science
The lemma is invoked directly by parityOf_cons to obtain the recursive rule parityOf (v :: vs) = a v XOR parityOf vs. That rule in turn supports the definitions of satisfiesXOR and SatisfiableXOR, which encode parity constraints inside the broader SAT formalization. Within the Recognition Science development the result supplies a basic algebraic identity needed for any later reduction that treats XOR parity as a primitive constraint.
scope and limits
- Does not establish satisfiability of any concrete XOR system.
- Does not generalize the identity to operations other than Boolean XOR.
- Does not depend on the numerical value of $n$ or on the particular assignment $a$.
- Does not supply complexity bounds for evaluating the fold.
Lean usage
unfold parityOf; simp only [List.foldl_cons]; rw [foldl_xor_init]; rw [Bool.false_xor, Bool.xor_comm]formal statement (Lean)
60lemma foldl_xor_init {n} (a : Assignment n) (init : Bool) (vs : List (Var n)) :
61 vs.foldl (fun acc v => Bool.xor acc (a v)) init =
62 Bool.xor init (vs.foldl (fun acc v => Bool.xor acc (a v)) false) := by
proof body
Term-mode proof.
63 induction vs generalizing init with
64 | nil => simp
65 | cons v vs ih =>
66 simp only [List.foldl_cons]
67 rw [ih (Bool.xor init (a v)), ih (Bool.xor false (a v))]
68 simp only [Bool.false_xor]
69 rw [Bool.xor_assoc]
70
71/-- Parity of cons: XOR of head and tail parity -/