internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof state before:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
ih : (List.foldl insertUnit (hd_res.fst, hd_res.snd.fst, hd_res.snd.snd) tl).snd.fst.size = hd_res.snd.fst.size
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size
Tactic:
simp only [Prod.mk.eta] at ih
Proof state after:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
ih : (List.foldl insertUnit hd_res tl).snd.fst.size = hd_res.snd.fst.size
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size
Theorem: LRAT.DefaultFormula.insertUnit_fold_preserves_size
Proof state before:
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
ih : (List.foldl insertUnit hd_res tl).snd.fst.size = hd_res.snd.fst.size
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size
Tactic:
rw [ih, insertUnit_preserves_size]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (f.insertRupUnits units).fst.assignments.size = f.assignments.size
Tactic:
simp only [insertRupUnits, Prod.mk.eta]
Proof state after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst.size = f.assignments.size
Theorem: LRAT.DefaultFormula.insertRupUnits_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst.size = f.assignments.size
Tactic:
exact insertUnit_fold_preserves_size f.rupUnits f.assignments false
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_preserves_clauses
Proof state before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (f.insertRupUnits units).fst.clauses = f.clauses
Tactic:
rw [insertRupUnits]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_preserves_ratUnits
Proof state before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (f.insertRupUnits units).fst.ratUnits = f.ratUnits
Tactic:
rw [insertRupUnits]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
⊢ update_res.snd.fst.size = n
Tactic:
rw [insertUnit_preserves_size]
Proof state after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
⊢ assignments.size = n
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
⊢ assignments.size = n
Tactic:
exact assignments_size
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
⊢ insertUnit_invariant assignments0 assignments0_size units assignments assignments_size →
    let update_res := insertUnit (units, assignments, foundContradiction) l;
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
intro h
Proof state after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
h : insertUnit_invariant assignments0 assignments0_size units assignments assignments_size
⊢ let update_res := insertUnit (units, assignments, foundContradiction) l;
  let_fun update_res_size := ⋯;
  insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
h : insertUnit_invariant assignments0 assignments0_size units assignments assignments_size
⊢ let update_res := insertUnit (units, assignments, foundContradiction) l;
  let_fun update_res_size := ⋯;
  insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Tactic:
simp only [insertUnit_invariant, Fin.getElem_fin, ne_eq, Bool.not_eq_true] at h
Proof state after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
h :
  ∀ (i : Fin n),
    (assignments[↑i] = assignments0[↑i] ∧ ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i) ∨
      (∃ j b i_gt_zero,
          units[↑j] = (⟨↑i, ⋯⟩, b) ∧
            assignments[↑i] = addAssignment b assignments0[↑i] ∧
              hasAssignment b assignments0[↑i] = false ∧ ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i) ∨
        ∃ j1 j2 i_gt_zero,
          units[↑j1] = (⟨↑i, ⋯⟩, true) ∧
            units[↑j2] = (⟨↑i, ⋯⟩, false) ∧
              assignments[↑i] = both ∧
                assignments0[↑i] = unassigned ∧ ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
⊢ let update_res := insertUnit (units, assignments, foundContradiction) l;
  let_fun update_res_size := ⋯;
  insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
h :
  (assignments[↑i] = assignments0[↑i] ∧ ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i) ∨
    (∃ j b i_gt_zero,
        units[↑j] = (⟨↑i, ⋯⟩, b) ∧
          assignments[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧ ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        units[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          units[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments[↑i] = both ∧
              assignments0[↑i] = unassigned ∧ ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
⊢ ↑i < assignments.size
Tactic:
omega
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
h :
  (assignments[↑i] = assignments0[↑i] ∧ ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i) ∨
    (∃ j b i_gt_zero,
        units[↑j] = (⟨↑i, ⋯⟩, b) ∧
          assignments[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧ ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        units[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          units[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments[↑i] = both ∧
              assignments0[↑i] = unassigned ∧ ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
i_in_bounds : ↑i < assignments.size
⊢ l.fst.val < assignments.size
Tactic:
rw [assignments_size]
Proof state after:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
h :
  (assignments[↑i] = assignments0[↑i] ∧ ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i) ∨
    (∃ j b i_gt_zero,
        units[↑j] = (⟨↑i, ⋯⟩, b) ∧
          assignments[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧ ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        units[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          units[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments[↑i] = both ∧
              assignments0[↑i] = unassigned ∧ ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
i_in_bounds : ↑i < assignments.size
⊢ l.fst.val < n
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
h :
  (assignments[↑i] = assignments0[↑i] ∧ ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i) ∨
    (∃ j b i_gt_zero,
        units[↑j] = (⟨↑i, ⋯⟩, b) ∧
          assignments[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧ ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        units[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          units[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments[↑i] = both ∧
              assignments0[↑i] = unassigned ∧ ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
i_in_bounds : ↑i < assignments.size
⊢ l.fst.val < n
Tactic:
exact l.1.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case pos
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ((insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
      ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
        ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i) ∨
    (∃ j b i_gt_zero,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j] = (⟨↑i, ⋯⟩, b) ∧
          (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧
              ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                ¬k = j → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          (insertUnit (units, assignments, foundContradiction) l).fst[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = both ∧
              assignments0[↑i] = unassigned ∧
                ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                  ¬k = j1 → ¬k = j2 → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i
Tactic:
next h3 =>
apply Or.inl
simp only [insertUnit, h3, Prod.mk.eta, ite_true]
constructor
. exact h1
. intro j
  have hsize : (insertUnit (units, assignments, foundContradiction) l).1.size = units.size := by
    simp [insertUnit, h3]
  let j' : Fin (Array.size units) := ⟨j.1, by rw [← hsize]; exact j.2⟩
  exact h2 j'
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ((insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
      ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
        ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i) ∨
    (∃ j b i_gt_zero,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j] = (⟨↑i, ⋯⟩, b) ∧
          (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = addAssignment b assignments0[↑i] ∧
            hasAssignment b assignments0[↑i] = false ∧
              ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                ¬k = j → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        (insertUnit (units, assignments, foundContradiction) l).fst[↑j1] = (⟨↑i, ⋯⟩, true) ∧
          (insertUnit (units, assignments, foundContradiction) l).fst[↑j2] = (⟨↑i, ⋯⟩, false) ∧
            (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = both ∧
              assignments0[↑i] = unassigned ∧
                ∀ (k : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
                  ¬k = j1 → ¬k = j2 → ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i
Tactic:
apply Or.inl
Proof state after:
case h
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
    ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
      ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case h
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ (insertUnit (units, assignments, foundContradiction) l).snd.fst[↑i] = assignments0[↑i] ∧
    ∀ (j : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size),
      ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑j].fst.val = ↑i
Tactic:
simp only [insertUnit, h3, Prod.mk.eta, ite_true]
Proof state after:
case h
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ assignments[↑i] = assignments0[↑i] ∧
    ∀
      (j :
        Fin
          (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
              else
                (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                  foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
      ¬units[↑j].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case h
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ assignments[↑i] = assignments0[↑i] ∧
    ∀
      (j :
        Fin
          (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
              else
                (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                  foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
      ¬units[↑j].fst.val = ↑i
Tactic:
constructor
Proof state after:
case h.left
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ assignments[↑i] = assignments0[↑i]

case h.right
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ∀
    (j :
      Fin
        (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
            else
              (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
    ¬units[↑j].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case h.left
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ assignments[↑i] = assignments0[↑i]

case h.right
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ∀
    (j :
      Fin
        (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
            else
              (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
    ¬units[↑j].fst.val = ↑i
Tactic:
. exact h1
Proof state after:
case h.right
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ∀
    (j :
      Fin
        (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
            else
              (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
    ¬units[↑j].fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case h.right
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ ∀
    (j :
      Fin
        (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
            else
              (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
    ¬units[↑j].fst.val = ↑i
Tactic:
. intro j
  have hsize : (insertUnit (units, assignments, foundContradiction) l).1.size = units.size := by
    simp [insertUnit, h3]
  let j' : Fin (Array.size units) := ⟨j.1, by rw [← hsize]; exact j.2⟩
  exact h2 j'
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case h.left
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ assignments[↑i] = assignments0[↑i]
Tactic:
exact h1
Proof state after:
no goals