internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.data

case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
. rw [l'_eq_l'']
  exact Or.inl l''_in_l
Proof state after:
case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
. exact h l' l'_in_acc
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
rw [l'_eq_l'']
Proof state after:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l'' ∈ l ∨ l'' ∈ units.data
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l'' ∈ l ∨ l'' ∈ units.data
Tactic:
exact Or.inl l''_in_l
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.mem_insertUnit_fold_units
Proof state before:
case inr
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_in_acc : l' ∈ acc.fst.data
⊢ l' ∈ l ∨ l' ∈ units.data
Tactic:
exact h l' l'_in_acc
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
⊢ (f.insertRupUnits c.negate).snd = true → p ⊨ c
Tactic:
simp only [insertRupUnits]
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true → p ⊨ c
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true → p ⊨ c
Tactic:
intro insertUnit_fold_success
Proof 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
⊢ p ⊨ c
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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
⊢ p ⊨ c
Tactic:
have false_imp : false → ∃ i : PosFin n, f.assignments[i.1]'(by rw [f_readyForRupAdd.2.1]; exact i.2.2) = both := by
  intro h
  simp only at h
Proof 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
⊢ p ⊨ c
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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
⊢ p ⊨ c
Tactic:
rcases contradiction_of_insertUnit_fold_success f.assignments f_readyForRupAdd.2.1 f.rupUnits false (negate c) false_imp
  insertUnit_fold_success with ⟨i, hboth⟩
Proof state after:
case 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
⊢ p ⊨ c
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
case 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
⊢ p ⊨ c
Tactic:
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
Proof state after:
case 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
⊢ p ⊨ c
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
case 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
⊢ p ⊨ c
Tactic:
have h0 : insertUnit_invariant f.assignments f_readyForRupAdd.2.1 f.rupUnits f.assignments f_readyForRupAdd.2.1 := by
  intro i
  simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
  apply Or.inl
  intro j
  simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j
  exact Fin.elim0 j
Proof state after:
case 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 ⋯
⊢ p ⊨ c
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
case 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 ⋯
⊢ p ⊨ c
Tactic:
have insertUnit_fold_satisfies_invariant := insertUnit_fold_preserves_invariant f.assignments f_readyForRupAdd.2.1 f.rupUnits
  f.assignments f_readyForRupAdd.2.1 false (negate c) h0
Proof state after:
case 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
⊢ p ⊨ c
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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
i : PosFin n
⊢ i.val < f.assignments.size
Tactic:
rw [f_readyForRupAdd.2.1]
Proof 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
i : PosFin n
⊢ i.val < n
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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
i : PosFin n
⊢ i.val < n
Tactic:
exact i.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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 = true → ∃ i, f.assignments[i.val] = both
Tactic:
intro h
Proof 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
h : false = true
⊢ ∃ i, f.assignments[i.val] = both
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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
h : false = true
⊢ ∃ i, f.assignments[i.val] = both
Tactic:
simp only at h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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.val < f.assignments.size
Tactic:
rw [f_readyForRupAdd.2.1]
Proof 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.val < n
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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.val < n
Tactic:
exact i.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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
⊢ insertUnit_invariant f.assignments ⋯ f.rupUnits f.assignments ⋯
Tactic:
intro i
Proof 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
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.rupUnits.size), f.rupUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.rupUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.rupUnits.size), k ≠ j → f.rupUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), k ≠ j1 → k ≠ j2 → f.rupUnits[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.rupUnits.size), f.rupUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.rupUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.rupUnits.size), k ≠ j → f.rupUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), k ≠ j1 → k ≠ j2 → f.rupUnits[k].fst.val ≠ ↑i
Tactic:
simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
Proof 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
i : Fin n
⊢ (∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i) ∨
    (∃ j b,
        (∃ x, f.rupUnits[↑j] = (⟨↑i, ⋯⟩, b)) ∧
          f.assignments[↑i] = addAssignment b f.assignments[↑i] ∧
            hasAssignment b f.assignments[↑i] = false ∧
              ∀ (k : Fin f.rupUnits.size), ¬k = j → ¬f.rupUnits[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            f.assignments[↑i] = both ∧
              f.assignments[↑i] = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), ¬k = j1 → ¬k = j2 → ¬f.rupUnits[↑k].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof 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
i : Fin n
⊢ (∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i) ∨
    (∃ j b,
        (∃ x, f.rupUnits[↑j] = (⟨↑i, ⋯⟩, b)) ∧
          f.assignments[↑i] = addAssignment b f.assignments[↑i] ∧
            hasAssignment b f.assignments[↑i] = false ∧
              ∀ (k : Fin f.rupUnits.size), ¬k = j → ¬f.rupUnits[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.rupUnits[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          f.rupUnits[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            f.assignments[↑i] = both ∧
              f.assignments[↑i] = unassigned ∧
                ∀ (k : Fin f.rupUnits.size), ¬k = j1 → ¬k = j2 → ¬f.rupUnits[↑k].fst.val = ↑i
Tactic:
apply Or.inl
Proof state after:
case h
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
i : Fin n
⊢ ∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
case h
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
i : Fin n
⊢ ∀ (j : Fin f.rupUnits.size), ¬f.rupUnits[↑j].fst.val = ↑i
Tactic:
intro j
Proof state after:
case h
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
i : Fin n
j : Fin f.rupUnits.size
⊢ ¬f.rupUnits[↑j].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
case h
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
i : Fin n
j : Fin f.rupUnits.size
⊢ ¬f.rupUnits[↑j].fst.val = ↑i
Tactic:
simp only [f_readyForRupAdd.1, Array.size_toArray, List.length_nil] at j
Proof state after:
case h
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
i : Fin n
j✝ : Fin f.rupUnits.size
j : Fin 0
⊢ ¬f.rupUnits[↑j✝].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertRup_entails_hsat
Proof state before:
case h
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
i : Fin n
j✝ : Fin f.rupUnits.size
j : Fin 0
⊢ ¬f.rupUnits[↑j✝].fst.val = ↑i
Tactic:
exact Fin.elim0 j
Proof state after:
no goals