clauseUnit_correct

formal source

 308    - For .neg v: the literal is true iff a v = false
 309
 310    **Status**: PROVED (formerly axiom) -/
 311theorem clauseUnit_correct {n} (σ : PartialAssignment n) (a : Assignment n) (C : Clause n)
 312    (v : Var n) (b : Bool)
 313    (hcompat : compatible σ a)
 314    (hsat : evalClause a C = true)
 315    (hmiss : clauseUnit σ C = some (v, b)) :
 316    b = a v := by
 317  unfold clauseUnit at hmiss
 318  simp only at hmiss
 319
 320  split at hmiss
 321  case isFalse h => simp at hmiss
 322  case isTrue h_len1 =>
 323    split at hmiss
 324    case isFalse h => simp at hmiss
 325    case isTrue h_all_false =>
 326      -- Set up unknowns
 327      set unknowns := (C.zip (C.map (valueOfLit σ))).filter (fun ⟨_, o⟩ => o.isNone) with hunk_def
 328      have h_len1' : unknowns.length = 1 := h_len1
 329
 330      -- Get the singleton element
 331      obtain ⟨unk, h_singleton, hunk_get⟩ := singleton_eq_get_zero' unknowns h_len1'
 332
 333      -- Known literals are false
 334      have h_known_false : ∀ l ∈ C, (valueOfLit σ l).isSome → evalLit a l = false := by
 335        intro l hl_in hsome
 336        have hval_in : valueOfLit σ l ∈ (C.map (valueOfLit σ)).filter Option.isSome := by
 337          simp only [List.mem_filter, List.mem_map]
 338          exact ⟨⟨l, hl_in, rfl⟩, hsome⟩
 339        rw [List.all_eq_true] at h_all_false
 340        simp only [decide_eq_true_eq] at h_all_false
 341        exact known_lit_false'' σ a l hcompat hsome (h_all_false _ hval_in)