Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
case intro.inl.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
h1 :
  (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[↑⟨i.val, ⋯⟩] = f.assignments[↑⟨i.val, ⋯⟩]
h2 :
  ∀ (j : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size),
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j].fst.val ≠ ↑⟨i.val, ⋯⟩
⊢ p ⊨ c

case intro.inr.inl.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h2 :
  (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[↑⟨i.val, ⋯⟩] =
    addAssignment b f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
⊢ p ⊨ c

case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j1 j2 : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j1] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)
h2 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j2] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
left✝¹ : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j1 → k ≠ j2 → (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
⊢ p ⊨ c
Tactic:
. rw [h1] at hboth
  simp only at hboth
  have hpos : hasAssignment true (f.assignments[i.1]'i_in_bounds) = true := by simp only [hboth]; decide
  have hneg : hasAssignment false (f.assignments[i.1]'i_in_bounds) = true := by simp only [hboth]; decide
  have p_entails_i_true := (assignments_invariant_of_strong_assignments_invariant f f_readyForRupAdd.2).2 i true hpos p pf
  have p_entails_i_false := (assignments_invariant_of_strong_assignments_invariant f f_readyForRupAdd.2).2 i false hneg p pf
  simp only [HSat.eval] at p_entails_i_true p_entails_i_false
  simp only [p_entails_i_true] at p_entails_i_false
Proof state after:
case intro.inr.inl.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size
b : Bool
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, b)
h2 :
  (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[↑⟨i.val, ⋯⟩] =
    addAssignment b f.assignments[↑⟨i.val, ⋯⟩]
h3 : ¬hasAssignment b f.assignments[↑⟨i.val, ⋯⟩] = true
h4 :
  ∀ (k : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j → (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
⊢ p ⊨ c

case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
false_imp : false = true → ∃ i, f.assignments[i.val] = both
i : PosFin n
hboth : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
h0 : insertUnit_invariant f.assignments ⋯ f.rupUnits f.assignments ⋯
insertUnit_fold_satisfies_invariant :
  let update_res := List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate;
  let_fun update_res_size := ⋯;
  insertUnit_invariant f.assignments ⋯ update_res.fst update_res.snd.fst update_res_size
j1 j2 : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j1] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, true)
h2 : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j2] = (⟨↑⟨i.val, ⋯⟩, ⋯⟩, false)
left✝¹ : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).snd.fst[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.size),
    k ≠ j1 → k ≠ j2 → (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[k].fst.val ≠ ↑⟨i.val, ⋯⟩
⊢ p ⊨ c