setVar_same
Updating a partial assignment at index v to boolean b returns some b on lookup at v. Researchers formalizing SAT backpropagation or monotone state updates cite this basic property when proving preservation of determined values. The proof is a one-line wrapper that unfolds the setVar definition and applies simplification.
claimLet $n$ be a natural number, let $σ : Var(n) → Option(Bool)$ be a partial assignment, let $v ∈ Var(n)$, and let $b ∈ Bool$. Then $(setVar(σ, v, b))(v) = some(b)$.
background
PartialAssignment n is the type of functions from Var n (Fin n indices) to Option Bool, with none denoting an unknown value and some b a determined boolean. The setVar operation is the pointwise update that replaces the entry at v with some b while leaving all other entries unchanged. The module develops backpropagation over CNF formulas augmented with XOR constraints, using these partial assignments to track literals whose values become forced during inference.
proof idea
The proof is a one-line wrapper. It unfolds the definition of setVar (the lambda that returns some b precisely when the queried index equals v) and applies simp to discharge the resulting equality.
why it matters in Recognition Science
The lemma supplies the core update semantics required by bp_step_monotone (which shows that backpropagation steps never unassign already-known values) and by compatible_setVar (which shows that setting a variable to its value in a compatible full assignment preserves compatibility). It therefore anchors the state-transition invariants used throughout the SAT backpropagation development.
scope and limits
- Does not state the value returned at any index other than v.
- Does not address repeated applications of setVar.
- Does not connect the update to satisfaction of the underlying CNF or XOR system.
Lean usage
example {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) : setVar σ v b v = some b := by simp [setVar_same]formal statement (Lean)
20@[simp] lemma setVar_same {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) :
21 setVar σ v b v = some b := by
proof body
One-line wrapper that applies unfold.
22 unfold setVar; simp
23