theorem
proved
tactic proof
clauseUnit_correct
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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)
342
343 -- Some literal is true
344 rw [evalClause, List.any_eq_true] at hsat
345 obtain ⟨l_sat, hl_in, hl_true⟩ := hsat
346
347 -- l_sat must be unknown
348 have hl_unknown : (valueOfLit σ l_sat).isNone := by
349 rw [← not_isSome_iff_isNone']
350 intro hsome
351 have hfalse := h_known_false l_sat hl_in hsome
352 rw [hl_true] at hfalse
353 cases hfalse
354
355 -- l_sat is in unknowns
356 have hl_in_unk : (l_sat, valueOfLit σ l_sat) ∈ unknowns := by
357 rw [hunk_def, List.mem_filter]
358 constructor
359 · have hlen : C.length = (C.map (valueOfLit σ)).length := by simp
360 obtain ⟨i, hi, hget⟩ := List.mem_iff_getElem.mp hl_in
361 have hi2 : i < (C.map (valueOfLit σ)).length := by simp; omega
362 have hmem := mem_zip_of_getElem' C (C.map (valueOfLit σ)) i hi hi2
363 simp only [List.getElem_map, hget] at hmem
364 exact hmem
365 · exact hl_unknown
366
367 -- Since unknowns = [unk], l_sat = unk.fst
368 rw [h_singleton, List.mem_singleton] at hl_in_unk
369 have hl_eq : l_sat = unk.fst := congrArg Prod.fst hl_in_unk
370
371 -- Rewrite hmiss using hunk_get
372 have hmiss' : (match unk.fst with
373 | .pos v => some (v, true)
374 | .neg v => some (v, false)) = some (v, b) := by
375 convert hmiss using 2
376 rw [← hunk_get]
377
378 -- Case analysis on unk.fst
379 cases hl : unk.fst with
380 | pos w =>
381 simp only [hl] at hmiss'
382 simp only [Option.some.injEq, Prod.mk.injEq] at hmiss'
383 obtain ⟨hv_eq, hb_eq⟩ := hmiss'
384 subst hv_eq hb_eq
385 rw [hl_eq, hl] at hl_true
386 simp only [evalLit] at hl_true
387 exact hl_true.symm
388
389 | neg w =>
390 simp only [hl] at hmiss'
391 simp only [Option.some.injEq, Prod.mk.injEq] at hmiss'
392 obtain ⟨hv_eq, hb_eq⟩ := hmiss'
393 subst hv_eq hb_eq
394 rw [hl_eq, hl] at hl_true
395 simp only [evalLit, Bool.not_eq_true'] at hl_true
396 exact hl_true.symm
397-- ... 3 more lines elided ...