theorem
proved
tactic proof
xorMissing_correct
show as:
view Lean formalization →
formal statement (Lean)
213theorem xorMissing_correct {n} (σ : PartialAssignment n) (a : Assignment n) (X : XORConstraint n)
214 (v : Var n) (b : Bool)
215 (hcompat : compatible σ a)
216 (hsat : satisfiesXOR a X)
217 (hmiss : xorMissing σ X = some (v, b)) :
218 b = a v := by
proof body
Tactic-mode proof.
219 unfold xorMissing at hmiss
220 simp only at hmiss
221 split at hmiss
222 case isTrue h_len1 =>
223 simp only [Option.some.injEq, Prod.mk.injEq] at hmiss
224 obtain ⟨hv_eq, hb_eq⟩ := hmiss
225
226 set unknowns := X.vars.filter (fun w => (σ w).isNone) with h_unknowns_def
227 set known := X.vars.filter (fun w => (σ w).isSome) with h_known_def
228
229 have h_unknowns_singleton : unknowns = [v] := by
230 have h := list_singleton_of_length_one' unknowns h_len1
231 rw [h, hv_eq]
232
233 unfold satisfiesXOR at hsat
234
235 have h_split := parityOf_filter_split' a X.vars (fun w => (σ w).isSome)
236 have h_filter_eq : X.vars.filter (fun w => !(σ w).isSome) = unknowns := by
237 simp only [h_unknowns_def]; congr 1; ext w; exact not_isSome_eq_isNone' (σ w)
238 rw [h_filter_eq, h_unknowns_singleton] at h_split
239
240 have h_par_v : parityOf a [v] = a v := by simp [parityOf]
241 rw [h_par_v, ← h_known_def] at h_split
242 rw [hsat] at h_split
243
244 have h_known_par := knownParity_eq_parityOf_known' σ a X hcompat
245 rw [← h_known_def] at h_known_par
246
247 rw [← hb_eq, h_known_par, h_split]
248 exact xor_comm_cancel' (a v) (parityOf a known)
249
250 case isFalse h => simp at hmiss
251
252/-!
253## Semantic Correctness for Unit Propagation
254
255The clauseUnit function produces the correct value for a satisfying assignment.
256This is now a **proved theorem**, not an axiom.
257-/
258
259-- Helper lemmas for clauseUnit_correct proof