internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case isTrue
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ units.size < (units, assignments, foundContradiction).fst.size

case isFalse
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
⊢ units.size <
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.size
Tactic:
. contradiction
Proof state after:
case isFalse
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
⊢ units.size <
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.size
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case isFalse
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
⊢ units.size <
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.size
Tactic:
. simp only [Array.size_push, Nat.lt_succ_self]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case isTrue
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
⊢ units.size < (units, assignments, foundContradiction).fst.size
Tactic:
contradiction
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case isFalse
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
⊢ units.size <
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.size
Tactic:
simp only [Array.size_push, Nat.lt_succ_self]
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
⊢ ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
Tactic:
simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push]
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
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
⊢ ↑j < units.size + 1
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h1 : units[↑j] = (⟨↑i, ⋯⟩, b)
h2 : assignments[↑i] = addAssignment b assignments0[↑i]
h3 : hasAssignment b assignments0[↑i] = false
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
⊢ ↑j < units.size + 1
Tactic:
exact Nat.lt_trans j.2 (Nat.lt_succ_self units.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)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = true
⊢ ∃ 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:
exfalso
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
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = true
⊢ False
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = true
⊢ False
Tactic:
have assignments_i_rw : assignments[i.1]! = assignments[i.1] := by
  simp only [getElem!, i_in_bounds, ↓reduceDite, Array.get_eq_getElem]
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
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = true
assignments_i_rw : assignments[↑i]! = assignments[↑i]
⊢ False
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = true
assignments_i_rw : assignments[↑i]! = assignments[↑i]
⊢ False
Tactic:
rw [hl, ← i_eq_l, assignments_i_rw, h2] at h5
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
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment true (addAssignment true assignments0[↑i]) = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = true
assignments_i_rw : assignments[↑i]! = assignments[↑i]
⊢ False
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment true (addAssignment true assignments0[↑i]) = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = true
assignments_i_rw : assignments[↑i]! = assignments[↑i]
⊢ False
Tactic:
exact h5 (has_of_add _ true)
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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = true
⊢ assignments[↑i]! = assignments[↑i]
Tactic:
simp only [getElem!, i_in_bounds, ↓reduceDite, Array.get_eq_getElem]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case 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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = false
⊢ l = (⟨↑i, ⋯⟩, false) ∧
    (assignments.modify l.fst.val (addAssignment l.snd))[↑i] = both ∧
      assignments0[↑i] = unassigned ∧
        ∀
          (k :
            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),
          ¬k = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬k = mostRecentUnitIdx → ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
. constructor
  . simp only [i_eq_l, ← hl]
    apply Prod.mk.eta
  . constructor
    . simp only [i_eq_l]
      rw [Array.get_modify_at_idx l_in_bounds]
      simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
      apply addNeg_of_addPos_eq_both
    . constructor
      . match h : assignments0[i.val]'_ with
        | unassigned => rfl
        | pos => simp (config := {decide := true}) [h] at h3
        | neg =>
          simp only [addAssignment, addPosAssignment, h, ite_true] at h2
          simp only [i_eq_l] at h2
          simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasNegAssignment] at h5
        | both => simp (config := {decide := true}) only [h] at h3
      . intro k k_ne_j k_ne_l
        rw [Array.get_push]
        by_cases h : k.1 < units.size
        . simp only [h, dite_true]
          have k_ne_j : ⟨k.1, h⟩ ≠ j := by
            intro k_eq_j
            simp only [← k_eq_j, not_true] at k_ne_j
          exact h4 ⟨k.1, h⟩ k_ne_j
        . exfalso
          have k_property := k.2
          simp only [insertUnit, h5, Prod.mk.eta, ite_false, Array.size_push] at k_property
          rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
          . exact h k_lt_units_size
          . simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
            exact k_ne_l rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case 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
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, true)
h2 : assignments[↑i] = addAssignment true assignments0[↑i]
h3 : hasAssignment true assignments0[↑i] = false
hb : b = true
hl : l.snd = false
⊢ (units.push l)[↑j] = (⟨↑i, ⋯⟩, true)
Tactic:
rw [Array.get_push_lt units l j.1 j.2, h1]
Proof state after:
no goals