known_lit_false''

formal source

 274  have hi : i < (l1.zip l2).length := by simp; omega
 275  exact ⟨i, hi, by simp⟩
 276
 277private lemma known_lit_false'' {n} (σ : PartialAssignment n) (a : Assignment n) (l : Lit n)
 278    (hcompat : compatible σ a) (hsome : (valueOfLit σ l).isSome)
 279    (hfalse : (valueOfLit σ l).getD false = false) :
 280    evalLit a l = false := by
 281  have heq : valueOfLit σ l = some (evalLit a l) := by
 282    cases l with
 283    | pos v =>
 284      simp only [valueOfLit, evalLit] at *
 285      rcases hcompat v with h | h
 286      · exact h
 287      · simp [h] at hsome
 288    | neg v =>
 289      simp only [valueOfLit, evalLit, Option.map] at *
 290      rcases hcompat v with h | h
 291      · simp [h]
 292      · simp [h] at hsome
 293  cases hv : valueOfLit σ l with
 294  | none => simp [hv] at hsome
 295  | some b =>
 296    simp only [hv, Option.getD_some] at hfalse heq
 297    simp only [Option.some.injEq] at heq
 298    rw [← heq, hfalse]
 299
 300/-- **PROVED**: clauseUnit produces the correct value for a satisfying assignment.
 301    If exactly one literal is unknown in clause C, all known literals are false,
 302    and a satisfies C, then the value returned by clauseUnit equals a v.
 303
 304    **Mathematical justification**: A clause is satisfied iff at least one literal is true.
 305    If all known literals are false under a (by compatibility), and a satisfies C,
 306    then the unknown literal must be the satisfying one.
 307    - For .pos v: the literal is true iff a v = true