bp_step_sound

formal source

 396        exact hl_true.symm
 397
 398/-- Soundness of one step: preserves compatibility with any model. -/
 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
 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