setVar_same
plain-language theorem explainer
The lemma records that updating a partial assignment at variable v with boolean b returns some b on query at v. Researchers modeling SAT backpropagation would cite this identity when tracking determined values. The proof is a one-line wrapper that unfolds the update definition and simplifies.
Claim. Let $n$ be a natural number, let $σ$ map each variable index in $Fin n$ to an optional boolean, let $v$ be a variable index, and let $b$ be a boolean. The function that replaces the value at $v$ with $b$ (leaving all other entries unchanged) satisfies that function applied to $v$ equals some $b$.
background
PartialAssignment n is the type of maps from Var n (i.e., Fin n) to Option Bool, with none denoting an undetermined variable and some b a fixed value. The setVar operation is defined by case distinction on the queried index: it returns some b exactly when the index equals the chosen variable and otherwise delegates to the original map. The module treats these partial maps as the state 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 identity is invoked by bp_step_monotone (which asserts that propagation steps preserve already-determined values) and by compatible_setVar (which shows preservation of compatibility with a total assignment). It supplies the elementary update rule inside the backpropagation layer of the SAT encoding, a component of the broader complexity analysis in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.