setVar_ne
plain-language theorem explainer
Updating a partial assignment at variable v to boolean b leaves its value at any distinct variable w unchanged. Researchers formalizing SAT solvers or backpropagation over CNF and XOR constraints cite this invariance when proving monotonicity of propagation steps. The proof is a direct term reduction that unfolds the update definition, simplifies the conditional equality, and obtains a contradiction from the distinctness hypothesis.
Claim. Let $n$ be a natural number, let $σ$ map each variable in $Var(n)$ to an optional boolean, let $v$ and $w$ be distinct variables, and let $b$ be a boolean. The partial assignment obtained by forcing $v$ to $b$ agrees with $σ$ at $w$.
background
A partial assignment is a function from variables (indices in Fin n) to Option Bool, where none marks an undetermined variable and some b marks a fixed value. The update operation returns a new function that yields some b exactly at the chosen variable and otherwise copies the input function. The module develops backward propagation over CNF formulas that also carry an XOR system, using these partial assignments to track determined literals during constraint solving.
proof idea
The term proof unfolds the update definition, which is an if-then-else on variable equality. Simplification with ite_eq_right_iff reduces the goal to the statement that w equals v. The absurd tactic then derives falsehood directly from the supplied inequality hypothesis.
why it matters
The result is invoked inside the monotonicity lemma for backpropagation steps and inside the compatibility preservation lemma for set updates. It therefore supports the correctness argument for the overall propagation procedure on SAT instances with XOR clauses. In the Recognition framework the lemma supplies a basic invariance needed for the complexity analysis of constraint satisfaction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.