setVar_same
plain-language theorem explainer
Updating a partial assignment at variable v to boolean b returns b upon query at v. Researchers modeling backpropagation over CNF formulas with XOR constraints cite this update invariance. The proof is a one-line wrapper that unfolds the definition of the update function and simplifies the conditional expression.
Claim. Let $n$ be a natural number, let $σ$ be a function from variables in $Fin n$ to $Option Bool$, let $v$ be a variable in $Fin n$, and let $b$ be a boolean. Then the function obtained by updating $σ$ at $v$ to return $b$ satisfies that its value at $v$ equals $some b$.
background
PartialAssignment n denotes the type of functions from Var n (i.e., Fin n) to Option Bool, where none marks an unknown value and some b marks a determined value. The setVar operation is defined to return some b at the chosen index v and to retain the original value at all other indices. The module situates these objects as the state representation for backward propagation over CNF formulas augmented with XOR constraints.
proof idea
The proof is a one-line wrapper that unfolds the definition of setVar and applies the simp tactic.
why it matters
The lemma supplies the basic invariance needed by bp_step_monotone (which establishes that propagation steps never unassign known values) and by compatible_setVar (which shows preservation of compatibility with a total assignment). It occupies a foundational position inside the backpropagation machinery for SAT instances with XOR constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.