Theorem: LRAT.DefaultFormula.insertRup_entails_hsat (LeanSAT/LRAT/Formula/RupAddSound.lean)

State before:
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)
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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = pos
h2 : both = both
⊢ hasAssignment true f.assignments[i.val] = true
Tactic:
simp only [hasAssignment, hasPosAssignment, ite_true, heq]
State after:
no goals

State before:
case intro.inr.inl.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.h.h_2
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)
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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq✝ : f.assignments[i.val] = neg
h2 : both = neg
⊢ p i = true
Tactic:
simp only at h2
State after:
no goals

State before:
case intro.inr.inl.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.h.h_3
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)
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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq✝ : f.assignments[i.val] = both
h2 : both = both
⊢ p i = true
Tactic:
next heq =>
exfalso
rw [heq] at h3
exact h3 (has_of_both b)
State after:
no goals

State before:
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)
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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ p i = true
Tactic:
exfalso
State after:
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)
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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False

State before:
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)
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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False
Tactic:
rw [heq] at h3
State after:
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)
h3 : ¬hasAssignment b both = 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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False

State before:
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)
h3 : ¬hasAssignment b both = 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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq : f.assignments[i.val] = both
h2 : both = both
⊢ False
Tactic:
exact h3 (has_of_both b)
State after:
no goals

State before:
case intro.inr.inl.intro.intro.intro.intro.intro.intro.intro.inr.intro.intro.h.h_4
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)
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, ⋯⟩
ib_in_insertUnit_fold : (i, b) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i' : PosFin n
i_true_in_c : (i, true) ∈ c.clause
i'_eq_i : i' = i
b_eq_false : false = b
a✝ : Assignment
heq✝ : f.assignments[i.val] = unassigned
h2 : both = neg
⊢ p i = true
Tactic:
simp only at h2
State after:
no goals

State before:
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:
exfalso
State after:
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, ⋯⟩
⊢ False

State before:
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, ⋯⟩
⊢ False
Tactic:
have i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
  have i_rw : i = ⟨i.1, i.2⟩ := rfl
  rw [i_rw, ← h1]
  apply List.get_mem
State after:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
⊢ False

State before:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
⊢ False
Tactic:
have i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) (negate c)).1.data := by
  have i_rw : i = ⟨i.1, i.2⟩ := rfl
  rw [i_rw, ← h2]
  apply List.get_mem
State after:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
⊢ False

State before:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i_false_in_insertUnit_fold : (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
⊢ False
Tactic:
simp only [f_readyForRupAdd.1, negate, negateLiteral] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
State after:
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, ⋯⟩
i_true_in_insertUnit_fold :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
⊢ False

State before:
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, ⋯⟩
i_true_in_insertUnit_fold :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
⊢ False
Tactic:
have i_true_in_insertUnit_fold :=
  mem_insertUnit_fold_units #[] f.assignments false (c.clause.map negateLiteral) (i, true) i_true_in_insertUnit_fold
State after:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, true) ∈ List.map negateLiteral c.clause ∨ (i, true) ∈ #[].data
⊢ False

State before:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, true) ∈ List.map negateLiteral c.clause ∨ (i, true) ∈ #[].data
⊢ False
Tactic:
have i_false_in_insertUnit_fold :=
  mem_insertUnit_fold_units #[] f.assignments false (c.clause.map negateLiteral) (i, false) i_false_in_insertUnit_fold
State after:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, true) ∈ List.map negateLiteral c.clause ∨ (i, true) ∈ #[].data
i_false_in_insertUnit_fold : (i, false) ∈ List.map negateLiteral c.clause ∨ (i, false) ∈ #[].data
⊢ False

State before:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, true) ∈ List.map negateLiteral c.clause ∨ (i, true) ∈ #[].data
i_false_in_insertUnit_fold : (i, false) ∈ List.map negateLiteral c.clause ∨ (i, false) ∈ #[].data
⊢ False
Tactic:
simp only [negateLiteral, List.mem_map, Prod.mk.injEq, Bool.not_eq_true', Prod.exists,
  exists_eq_right_right, exists_eq_right, Array.data_toArray, List.find?, List.not_mem_nil, or_false,
  Bool.not_eq_false'] at i_true_in_insertUnit_fold i_false_in_insertUnit_fold
State after:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
⊢ False

State before:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
⊢ False
Tactic:
have c_not_tautology := Clause.not_tautology c (i, true)
State after:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
c_not_tautology : ¬(i, true) ∈ Clause.toList c ∨ ¬negateLiteral (i, true) ∈ Clause.toList c
⊢ False

State before:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
c_not_tautology : ¬(i, true) ∈ c.toList ∨ ¬negateLiteral (i, true) ∈ c.toList
⊢ False
Tactic:
rw [DefaultClause.toList] at c_not_tautology
State after:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
c_not_tautology : ¬(i, true) ∈ c.clause ∨ ¬negateLiteral (i, true) ∈ c.clause
⊢ False

State before:
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
c_not_tautology : ¬(i, true) ∈ c.clause ∨ ¬negateLiteral (i, true) ∈ c.clause
⊢ False
Tactic:
rcases c_not_tautology with i_true_not_in_c | i_false_not_in_c
State after:
case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inl
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_true_not_in_c : ¬(i, true) ∈ c.clause
⊢ False

case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_false_not_in_c : ¬negateLiteral (i, true) ∈ c.clause
⊢ False

State before:
case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inl
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_true_not_in_c : ¬(i, true) ∈ c.clause
⊢ False

case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_false_not_in_c : ¬negateLiteral (i, true) ∈ c.clause
⊢ False
Tactic:
. exact i_true_not_in_c i_false_in_insertUnit_fold
State after:
case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_false_not_in_c : ¬negateLiteral (i, true) ∈ c.clause
⊢ False

State before:
case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_false_not_in_c : ¬negateLiteral (i, true) ∈ c.clause
⊢ False
Tactic:
. exact i_false_not_in_c i_true_in_insertUnit_fold
State after:
no goals

State before:
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, ⋯⟩
⊢ (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
Tactic:
have i_rw : i = ⟨i.1, i.2⟩ := rfl
State after:
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, ⋯⟩
i_rw : i = ⟨i.val, ⋯⟩
⊢ (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data

State before:
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, ⋯⟩
i_rw : i = ⟨i.val, ⋯⟩
⊢ (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
Tactic:
rw [i_rw, ← h1]
State after:
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, ⋯⟩
i_rw : i = ⟨i.val, ⋯⟩
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j1] ∈
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data

State before:
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, ⋯⟩
i_rw : i = ⟨i.val, ⋯⟩
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j1] ∈
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
Tactic:
apply List.get_mem
State after:
no goals

State before:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
⊢ (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
Tactic:
have i_rw : i = ⟨i.1, i.2⟩ := rfl
State after:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i_rw : i = ⟨i.val, ⋯⟩
⊢ (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data

State before:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i_rw : i = ⟨i.val, ⋯⟩
⊢ (i, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
Tactic:
rw [i_rw, ← h2]
State after:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i_rw : i = ⟨i.val, ⋯⟩
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j2] ∈
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data

State before:
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, ⋯⟩
i_true_in_insertUnit_fold : (i, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
i_rw : i = ⟨i.val, ⋯⟩
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst[j2] ∈
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).fst.data
Tactic:
apply List.get_mem
State after:
no goals

State before:
case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inl
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_true_not_in_c : ¬(i, true) ∈ c.clause
⊢ False
Tactic:
exact i_true_not_in_c i_false_in_insertUnit_fold
State after:
no goals

State before:
case intro.inr.inr.intro.intro.intro.intro.intro.intro.intro.inr
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, ⋯⟩
i_true_in_insertUnit_fold✝ :
  (i, true) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_false_in_insertUnit_fold✝ :
  (i, false) ∈ (List.foldl insertUnit (#[], f.assignments, false) (List.map negateLiteral c.clause)).fst.data
i_true_in_insertUnit_fold : (i, false) ∈ c.clause
i_false_in_insertUnit_fold : (i, true) ∈ c.clause
i_false_not_in_c : ¬negateLiteral (i, true) ∈ c.clause
⊢ False
Tactic:
exact i_false_not_in_c i_true_in_insertUnit_fold
State after:
no goals