lemma
proved
tactic proof
bp_step_sound
show as:
view Lean formalization →
formal statement (Lean)
399lemma bp_step_sound {n} (φ : CNF n) (H : XORSystem n)
400 {s t : BPState n} :
401 BPStep φ H s t →
402 ∀ a : Assignment n, evalCNF a φ = true → satisfiesSystem a H →
403 compatible s.assign a → compatible t.assign a := by
proof body
Tactic-mode proof.
404 intro hstep a hφ hH hcompat
405 cases hstep with
406 | xor_push X v b hX hmiss =>
407 -- Need to show: compatible (setVar s.assign v b) a
408 -- Since a satisfies X and xorMissing gave us (v, b), we need b = a v
409 have hXsat : satisfiesXOR a X := hH X hX
410 have hbeq : b = a v := xorMissing_correct s.assign a X v b hcompat hXsat hmiss
411 subst hbeq
412 exact compatible_setVar s.assign a v hcompat
413 | clause_unit C v b hC hmiss =>
414 -- Need to show: compatible (setVar s.assign v b) a
415 -- Since a satisfies C and clauseUnit gave us (v, b), we need b = a v
416 have hCsat : evalClause a C = true := by
417 unfold evalCNF at hφ
418 simp only [List.all_eq_true] at hφ
419 exact hφ C hC
420 have hbeq : b = a v := clauseUnit_correct s.assign a C v b hcompat hCsat hmiss
421 subst hbeq
422 exact compatible_setVar s.assign a v hcompat
423 | and_one => exact hcompat
424 | and_zero => exact hcompat
425 | or_one => exact hcompat
426 | or_zero => exact hcompat
427 | not_flip => exact hcompat
428 | wire_prop => exact hcompat
429
430/-- Monotonicity: steps never unassign known values. -/