internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.clear_insertRup
Proof state before:
case assignments.intro.h₂.inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
motive : Nat → Array Assignment → Prop := f.clear_insert_induction_motive ⋯ (f.insertRupUnits units).fst.rupUnits
h_base : motive 0 (f.insertRupUnits units).fst.assignments
h_inductive :
  ∀ (idx : Fin (f.insertRupUnits units).fst.rupUnits.size) (assignments : Array Assignment),
    motive (↑idx) assignments → motive (↑idx + 1) (clearUnit assignments (f.insertRupUnits units).fst.rupUnits[idx])
h_size :
  (Array.foldl (fun b => clearUnit b) (f.insertRupUnits units).fst.assignments (f.insertRupUnits units).fst.rupUnits
        0).size =
    n
i : Nat
hi1 : i < (Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits 0).size
hi2 : i < f.assignments.size
i_lt_n : i < n
h✝ :
  (∃ j b i_gt_zero,
      ↑j ≥ (f.insertRupUnits units).fst.rupUnits.size ∧
        (f.insertRupUnits units).fst.rupUnits[j] = (⟨↑⟨i, i_lt_n⟩, ⋯⟩, b) ∧
          (Array.foldl (fun b => clearUnit b) (f.insertRupUnits units).fst.assignments
                  (f.insertRupUnits units).fst.rupUnits 0)[↑⟨i, i_lt_n⟩] =
              addAssignment b f.assignments[↑⟨i, i_lt_n⟩] ∧
            ¬hasAssignment b f.assignments[↑⟨i, i_lt_n⟩] = true ∧
              ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
                ↑k ≥ (f.insertRupUnits units).fst.rupUnits.size →
                  k ≠ j → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨i, i_lt_n⟩) ∨
    ∃ j1 j2 i_gt_zero,
      ↑j1 ≥ (f.insertRupUnits units).fst.rupUnits.size ∧
        ↑j2 ≥ (f.insertRupUnits units).fst.rupUnits.size ∧
          (f.insertRupUnits units).fst.rupUnits[j1] = (⟨↑⟨i, i_lt_n⟩, ⋯⟩, true) ∧
            (f.insertRupUnits units).fst.rupUnits[j2] = (⟨↑⟨i, i_lt_n⟩, ⋯⟩, false) ∧
              (Array.foldl (fun b => clearUnit b) (f.insertRupUnits units).fst.assignments
                      (f.insertRupUnits units).fst.rupUnits 0)[↑⟨i, i_lt_n⟩] =
                  both ∧
                f.assignments[↑⟨i, i_lt_n⟩] = unassigned ∧
                  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
                    ↑k ≥ (f.insertRupUnits units).fst.rupUnits.size →
                      k ≠ j1 → k ≠ j2 → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨i, i_lt_n⟩
⊢ (Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits 0)[i] =
    f.assignments[i]
Tactic:
omega
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_clauses
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.clauses = f.clauses
Tactic:
simp only [performRupCheck, Misc.Prod.mk.eta]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_rupUnits
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.rupUnits = f.rupUnits
Tactic:
simp only [performRupCheck, Misc.Prod.mk.eta]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_ratUnits
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.ratUnits = f.ratUnits
Tactic:
simp only [performRupCheck, Misc.Prod.mk.eta]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_assignments_size
Proof state before:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
⊢ (confirmRupHint clauses (assignments, derivedLits, b1, b2) id).fst.size = assignments.size
Tactic:
simp only [confirmRupHint]
Proof state after:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
⊢ (if (b2 || b1) = true then (assignments, derivedLits, b1, b2)
        else
          match clauses[id]? with
          | some (some c) =>
            match c.reduce assignments with
            | ReduceResult.encounteredBoth => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToEmpty => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b assignments[l.val]! = true then (assignments, derivedLits, false, false)
              else (assignments.modify l.val (addAssignment b), (l, b) :: derivedLits, false, false)
            | ReduceResult.reducedToNonunit => (assignments, derivedLits, false, true)
          | some none => (assignments, derivedLits, false, true)
          | none => (assignments, derivedLits, false, true)).fst.size =
    assignments.size
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_assignments_size
Proof state before:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
⊢ (if (b2 || b1) = true then (assignments, derivedLits, b1, b2)
        else
          match clauses[id]? with
          | some (some c) =>
            match c.reduce assignments with
            | ReduceResult.encounteredBoth => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToEmpty => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b assignments[l.val]! = true then (assignments, derivedLits, false, false)
              else (assignments.modify l.val (addAssignment b), (l, b) :: derivedLits, false, false)
            | ReduceResult.reducedToNonunit => (assignments, derivedLits, false, true)
          | some none => (assignments, derivedLits, false, true)
          | none => (assignments, derivedLits, false, true)).fst.size =
    assignments.size
Tactic:
repeat first
  | rfl
  | simp only [Array.modify_preserves_size]
  | split
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_assignments_size
Proof state before:
case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Tactic:
first
| rfl
| simp only [Array.modify_preserves_size]
| split
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_assignments_size
Proof state before:
case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_assignments_size
Proof state before:
case isFalse.h_1.h_3.isFalse
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝¹ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
h✝ : ¬hasAssignment b✝ assignments[l✝.val]! = true
⊢ (assignments.modify l✝.val (addAssignment b✝), (l✝, b✝) :: derivedLits, false, false).fst.size = assignments.size

case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Tactic:
simp only [Array.modify_preserves_size]
Proof state after:
case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.assignments.size = f.assignments.size
Tactic:
simp only [performRupCheck, Prod.mk.eta]
Proof state after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst.size = f.assignments.size
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst.size = f.assignments.size
Tactic:
rw [Array.foldl_eq_foldl_data]
Proof state after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Tactic:
have hb : (f.assignments, ([] : List (Literal (PosFin n))), false, false).1.size = f.assignments.size := rfl
Proof state after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Tactic:
have hl (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
  (id : Nat) (_ : id ∈ rupHints.data) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
  have h := confirmRupHint_preserves_assignments_size f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
  simp only [Prod.mk.eta] at h
  rw [h, hsize]
Proof state after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
hl :
  ∀ (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    acc.fst.size = f.assignments.size →
      ∀ (id : Nat), id ∈ rupHints.data → (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
hl :
  ∀ (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    acc.fst.size = f.assignments.size →
      ∀ (id : Nat), id ∈ rupHints.data → (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
Tactic:
exact List.foldlRecOn rupHints.data (confirmRupHint f.clauses) (f.assignments, [], false, false) hb hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
Tactic:
have h := confirmRupHint_preserves_assignments_size f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
Proof state after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
h : (confirmRupHint f.clauses (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
h : (confirmRupHint f.clauses (acc.fst, acc.snd.fst, acc.snd.snd.fst, acc.snd.snd.snd) id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
Tactic:
simp only [Prod.mk.eta] at h
Proof state after:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
h : (confirmRupHint f.clauses acc id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = f.assignments.size
id : Nat
x✝ : id ∈ rupHints.data
h : (confirmRupHint f.clauses acc id).fst.size = acc.fst.size
⊢ (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
Tactic:
rw [h, hsize]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n
Tactic:
rw [Array.modify_preserves_size]
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ acc.fst.size = n
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ acc.fst.size = n
Tactic:
exact hsize
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ let_fun hsize' := ⋯;
  f.derivedLits_invariant f_assignments_size (acc.fst.modify l.fst.val (addAssignment l.snd)) hsize' (l :: acc.snd.fst)
Tactic:
intro _ i
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) Array.modify_preserves_size)) hsize
i : Fin n
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧ ∀ (l_1 : Literal (PosFin n)), l_1 ∈ l :: acc.snd.fst → l_1.fst.val ≠ ↑i) ∨
    (∃ j,
        ((l :: acc.snd.fst).get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((l :: acc.snd.fst).get j).snd fassignments_i ∧
            ¬hasAssignment ((l :: acc.snd.fst).get j).snd fassignments_i = true ∧
              ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ j → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((l :: acc.snd.fst).get j1).fst.val = ↑i ∧
          ((l :: acc.snd.fst).get j2).fst.val = ↑i ∧
            ((l :: acc.snd.fst).get j1).snd = true ∧
              ((l :: acc.snd.fst).get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ j1 → k ≠ j2 → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) Array.modify_preserves_size)) hsize
i : Fin n
⊢ ↑i < acc.fst.size
Tactic:
rw [hsize]
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) Array.modify_preserves_size)) hsize
i : Fin n
⊢ ↑i < n
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) Array.modify_preserves_size)) hsize
i : Fin n
⊢ ↑i < n
Tactic:
exact i.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) Array.modify_preserves_size)) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
⊢ l.fst.val < acc.fst.size
Tactic:
rw [hsize]
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) Array.modify_preserves_size)) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
⊢ l.fst.val < n
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) Array.modify_preserves_size)) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
⊢ l.fst.val < n
Tactic:
exact l.1.2.2
Proof state after:
no goals