internlm/Lean-Github huggingface dataset:
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
⊢ ∀
    (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 = mostRecentUnitIdx → ¬k = ⟨↑j, j_lt_updatedUnits_size⟩ → ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
intro k k_ne_l k_ne_j
Proof state after:
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
⊢ ¬(units.push l)[↑k].fst.val = ↑i
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
⊢ ¬(units.push l)[↑k].fst.val = ↑i
Tactic:
rw [Array.get_push]
Proof state after:
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
⊢ ¬(if h : ↑k < units.size then units[↑k] else l).fst.val = ↑i
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case neg
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ¬↑k < units.size
⊢ ¬(if h : ↑k < units.size then units[↑k] else l).fst.val = ↑i
Tactic:
. 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 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
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ↑k < units.size
⊢ ¬(if h : ↑k < units.size then units[↑k] else l).fst.val = ↑i
Tactic:
simp only [h, dite_true]
Proof state after:
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
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ↑k < units.size
⊢ ¬units[↑k].fst.val = ↑i
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
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ↑k < units.size
⊢ ¬units[↑k].fst.val = ↑i
Tactic:
have k_ne_j : ⟨k.1, h⟩ ≠ j := by
  intro k_eq_j
  simp only [← k_eq_j, not_true] at k_ne_j
Proof state after:
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
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j✝ : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ↑k < units.size
k_ne_j : ⟨↑k, h⟩ ≠ j
⊢ ¬units[↑k].fst.val = ↑i
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
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j✝ : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ↑k < units.size
k_ne_j : ⟨↑k, h⟩ ≠ j
⊢ ¬units[↑k].fst.val = ↑i
Tactic:
exact h4 ⟨k.1, h⟩ k_ne_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
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ↑k < units.size
⊢ ⟨↑k, h⟩ ≠ j
Tactic:
intro k_eq_j
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ↑k < units.size
k_eq_j : ⟨↑k, h⟩ = j
⊢ 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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ↑k < units.size
k_eq_j : ⟨↑k, h⟩ = j
⊢ False
Tactic:
simp only [← k_eq_j, not_true] at k_ne_j
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertUnit_preserves_invariant
Proof state before:
case neg
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ¬↑k < units.size
⊢ ¬(if h : ↑k < units.size then units[↑k] else l).fst.val = ↑i
Tactic:
exfalso
Proof state after:
case neg
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, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
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_ne_l : ¬k = mostRecentUnitIdx
k_ne_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
h : ¬↑k < units.size
⊢ False