internlm/Lean-Github huggingface dataset:
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
⊢ ((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.inr ∘ Or.inl
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
⊢ ∃ 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
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
⊢ ∃ 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
Tactic:
have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
  simp only [insertUnit, h5, Prod.mk.eta, ite_true]
  exact j.2
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ ∃ 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
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ ∃ 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
Tactic:
refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (insertUnit (units, assignments, foundContradiction) l).fst[↑⟨↑j, j_lt_updatedUnits_size⟩] = (⟨↑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, j_lt_updatedUnits_size⟩ →
            ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ (insertUnit (units, assignments, foundContradiction) l).fst[↑⟨↑j, j_lt_updatedUnits_size⟩] = (⟨↑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, j_lt_updatedUnits_size⟩ →
            ¬(insertUnit (units, assignments, foundContradiction) l).fst[↑k].fst.val = ↑i
Tactic:
simp only [insertUnit, h5, Prod.mk.eta, ite_true]
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ units[↑j] = (⟨↑i, ⋯⟩, b) ∧
    assignments[↑i] = addAssignment b assignments0[↑i] ∧
      hasAssignment b assignments0[↑i] = 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⟩ → ¬units[↑k].fst.val = ↑i
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ units[↑j] = (⟨↑i, ⋯⟩, b) ∧
    assignments[↑i] = addAssignment b assignments0[↑i] ∧
      hasAssignment b assignments0[↑i] = 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⟩ → ¬units[↑k].fst.val = ↑i
Tactic:
refine ⟨h1,h2,h3,?_⟩
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ ∀
    (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⟩ → ¬units[↑k].fst.val = ↑i
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ ∀
    (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⟩ → ¬units[↑k].fst.val = ↑i
Tactic:
intro k k_ne_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
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
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_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
⊢ ¬units[↑k].fst.val = ↑i
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
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_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
⊢ ¬units[↑k].fst.val = ↑i
Tactic:
have k_size : k.1 < units.size := by
  have k_property := k.2
  simp only [insertUnit, h5, Prod.mk.eta, ite_true] at k_property
  exact k_property
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
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_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
k_size : ↑k < units.size
⊢ ¬units[↑k].fst.val = ↑i
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
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_j : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
k_size : ↑k < units.size
⊢ ¬units[↑k].fst.val = ↑i
Tactic:
have k_ne_j : { val := k.val, isLt := k_size } ≠ j := by
  intro k_eq_j
  simp only [← Fin.val_eq_of_eq k_eq_j, not_true] at k_ne_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
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
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_j✝ : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
k_size : ↑k < units.size
k_ne_j : ⟨↑k, k_size⟩ ≠ j
⊢ ¬units[↑k].fst.val = ↑i
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
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
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_j✝ : ¬k = ⟨↑j, j_lt_updatedUnits_size⟩
k_size : ↑k < units.size
k_ne_j : ⟨↑k, k_size⟩ ≠ j
⊢ ¬units[↑k].fst.val = ↑i
Tactic:
exact h4 ⟨k.1, k_size⟩ 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
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
⊢ ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
Tactic:
simp only [insertUnit, h5, Prod.mk.eta, ite_true]
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
⊢ ↑j < units.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
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
⊢ ↑j < units.size
Tactic:
exact j.2
Proof state after:
no goals