knownParity_eq_parityOf_known'
plain-language theorem explainer
The lemma equates the foldl accumulation of known bits from a partial assignment σ to the parityOf computation over the filtered known variables under a compatible total assignment a. Researchers modeling XOR constraint propagation in SAT backpropagation would cite this equivalence. The proof proceeds by induction on the variable list of X, applying the compatibility extraction lemma at each known step and parityOf_cons for the reduction.
Claim. Let $σ$ be a partial assignment and $a$ a total assignment compatible with $σ$. For an XOR constraint $X$, the foldl over $X.vars$ that XORs the known values from $σ$ equals the parity of the known variables under $a$.
background
PartialAssignment n is the type of maps from variables to Option Bool, with none marking unknown bits and some b marking determined values. The predicate compatible σ a requires that σ and a agree wherever σ is defined. parityOf a S folds Bool.xor over a(v) for v in list S, starting from false. The upstream definition states that parityOf computes the XOR (parity) of selected variables of assignment a. The lemma also depends on getD_of_compat_isSome', which extracts a w from σ w when the latter is known under compatibility.
proof idea
The proof first proves a generalized claim for arbitrary initial accumulator by induction on X.vars. The nil case reduces directly via the definition of parityOf. For cons w ws, it cases on whether σ w is some: when known it substitutes the value via getD_of_compat_isSome', rewrites with the inductive hypothesis and parityOf_cons, then reassociates the xors; when unknown it drops the variable and applies the inductive hypothesis unchanged.
why it matters
This equivalence is invoked by xorMissing_correct to show that the value returned for a missing variable in an XOR constraint matches the satisfying assignment a. It supports the backpropagation mechanism for linear constraints over GF(2) inside the SAT encoding. The result fills a correctness step for partial assignment propagation in the complexity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.