compatible_setVar

formal source

 115  ∀ v, σ v = some (a v) ∨ σ v = none
 116
 117/-- If σ is compatible with a and we set v to (a v), the result is still compatible. -/
 118lemma compatible_setVar {n} (σ : PartialAssignment n) (a : Assignment n) (v : Var n)
 119    (hcompat : compatible σ a) :
 120    compatible (setVar σ v (a v)) a := by
 121  intro w
 122  by_cases hwv : w = v
 123  · subst hwv
 124    left
 125    simp [setVar_same]
 126  · rw [setVar_ne σ v w (a v) hwv]
 127    exact hcompat w
 128
 129/-!
 130## Semantic Correctness for XOR Propagation
 131
 132The xorMissing function produces the correct value for a satisfying assignment.
 133This is now a **proved theorem**, not an axiom.
 134-/
 135
 136-- Helper lemmas for xorMissing_correct proof
 137private lemma not_isSome_eq_isNone' {α : Type*} (o : Option α) : (!o.isSome) = o.isNone := by
 138  cases o <;> rfl
 139
 140private lemma xor_comm_assoc' (a b c : Bool) : Bool.xor a (Bool.xor b c) = Bool.xor b (Bool.xor a c) := by
 141  cases a <;> cases b <;> cases c <;> rfl
 142
 143private lemma xor_comm_cancel' (a b : Bool) : Bool.xor (Bool.xor b a) b = a := by
 144  cases a <;> cases b <;> rfl
 145
 146private lemma parityOf_filter_split' {n} (a : Assignment n) (vs : List (Var n)) (p : Var n → Bool) :
 147    parityOf a vs = Bool.xor
 148      (parityOf a (vs.filter p))