internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.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
⊢ (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]
    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 right.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
⊢ l = (⟨↑i, ⋯⟩, false)
Tactic:
simp only [i_eq_l, ← hl]
Proof state after:
case right.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
⊢ l = (⟨l.fst.val, ⋯⟩, l.snd)
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.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
⊢ l = (⟨l.fst.val, ⋯⟩, l.snd)
Tactic:
apply Prod.mk.eta
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.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
⊢ 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
  . 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 right.right.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
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[↑i] = both
Tactic:
simp only [i_eq_l]
Proof state after:
case right.right.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
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[l.fst.val] = both
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.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
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[l.fst.val] = both
Tactic:
rw [Array.get_modify_at_idx l_in_bounds]
Proof state after:
case right.right.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
⊢ addAssignment l.snd assignments[l.fst.val] = both
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.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
⊢ addAssignment l.snd assignments[l.fst.val] = both
Tactic:
simp only [addAssignment, hl, ← i_eq_l, h2, ite_true, ite_false]
Proof state after:
case right.right.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
⊢ assignments0[↑i].addPosAssignment.addNegAssignment = both
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.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
⊢ assignments0[↑i].addPosAssignment.addNegAssignment = both
Tactic:
apply addNeg_of_addPos_eq_both
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case right.right.right.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
⊢ ∀
    (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:
. 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 right.right.right.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
⊢ assignments0[↑i] = unassigned
Tactic:
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
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 = false
h : assignments0[↑i] = unassigned
⊢ unassigned = unassigned
Tactic:
rfl
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 = false
h : assignments0[↑i] = pos
⊢ pos = unassigned
Tactic:
simp (config := {decide := true}) [h] at h3
Proof state after:
no goals