Parity of Boolean lists

Executable exclusive-or folding agrees with addition in the Boolean ring and with the existing finite-tuple Cslib.parityOn. The empty word has parity zero. These bridges let list-based programs reuse the finite-coordinate parity API without changing the mathematical relation.

def Cslib.BitString.wordParity (word : List Bool) : Bool

Exclusive or of every bit, with zero for the empty word.

@[simp]

theorem Cslib.BitString.wordParity_nil : wordParity [] = false

@[simp]

theorem Cslib.BitString.wordParity_cons (b : Bool) (word : List Bool) : wordParity (b :: word) = (b ^^ wordParity word)

theorem Cslib.BitString.wordParity_eq_sum (word : List Bool) : wordParity word = word.sum

List parity is the sum in the existing Boolean ring.

theorem Cslib.BitString.wordParity_ofFn {n : ℕ} (x : Fin n → Bool) : wordParity (List.ofFn x) = parityOn Finset.univ x

Folding a finite tuple computes its existing finite-set parity.