internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case neg
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
h✝ : ¬l.fst.val = ↑i
⊢ 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
Tactic:
. next l_ne_i =>
  apply Or.inl
  constructor
  . rw [Array.get_modify_unchanged l_in_bounds i_in_bounds (addAssignment l.2) l_ne_i]
    exact h1
  . intro l' l'_in_list
    simp only [List.find?, List.mem_cons] at l'_in_list
    rcases l'_in_list with l'_eq_l | l'_in_acc
    . rw [l'_eq_l]
      exact l_ne_i
    . exact h2 l' l'_in_acc
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ 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
Tactic:
apply Or.inr ∘ Or.inl ∘ Exists.intro ⟨0, zero_lt_length_list⟩
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).fst.val = ↑i ∧
    (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
        addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] ∧
      ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
        ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((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_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).fst.val = ↑i ∧
    (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
        addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] ∧
      ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
        ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Tactic:
constructor
Proof state after:
case left
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).fst.val = ↑i

case right
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
      addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] ∧
    ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
      ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case left
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).fst.val = ↑i

case right
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
      addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] ∧
    ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
      ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Tactic:
. simp only [List.get, l_eq_i]
Proof state after:
case right
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
      addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] ∧
    ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
      ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case right
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
      addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] ∧
    ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
      ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Tactic:
. constructor
  . simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, List.get, h1]
  . constructor
    . simp only [List.get, Bool.not_eq_true]
      simp only [getElem!, l_in_bounds, ↓reduceDite, Array.get_eq_getElem,
        Bool.not_eq_true] at h
      simp only [l_eq_i, h1] at h
      exact h
    . intro k k_ne_zero
      have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
        have k_val_ne_zero : k.1 ≠ 0 := by
          intro k_eq_zero
          simp only [List.length_cons, Nat.succ_eq_add_one, Fin.zero_eta, ne_eq] at k_ne_zero
          apply k_ne_zero
          apply Fin.eq_of_val_eq
          simp [k_eq_zero]
        rcases Nat.exists_eq_succ_of_ne_zero k_val_ne_zero with ⟨k', k_eq_k'_succ⟩
        rw [Nat.succ_eq_add_one] at k_eq_k'_succ
        have k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length := by rw [← k_eq_k'_succ]; exact k.2
        apply Exists.intro k' ∘ Exists.intro k'_succ_in_bounds
        apply Fin.eq_of_val_eq
        exact k_eq_k'_succ
      rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩
      rw [k_eq_succ, List.get_cons_succ]
      have k'_in_bounds : k' < acc.2.1.length := by
        simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
        exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
      exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) $ List.get_mem acc.snd.fst k' k'_in_bounds
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
⊢ 0 < (l :: acc.snd.fst).length
Tactic:
simp only [List.length_cons]
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
⊢ 0 < acc.snd.fst.length.succ
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
⊢ 0 < acc.snd.fst.length.succ
Tactic:
exact Nat.zero_lt_succ (List.length acc.snd.fst)
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case left
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).fst.val = ↑i
Tactic:
simp only [List.get, l_eq_i]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case right
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
      addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] ∧
    ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
      ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Tactic:
constructor
Proof state after:
case right.left
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
    addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i]

case right.right
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
    ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case right.left
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd))[↑i] =
    addAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i]

case right.right
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
    ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i
Tactic:
. simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, List.get, h1]
Proof state after:
case right.right
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_in_bounds : l.fst.val < acc.fst.size
h1 : acc.fst[↑i] = f.assignments[↑i]
h2 : ∀ (l : Literal (PosFin n)), l ∈ acc.snd.fst → l.fst.val ≠ ↑i
l_eq_i : l.fst.val = ↑i
zero_lt_length_list : 0 < (l :: acc.snd.fst).length
⊢ ¬hasAssignment ((l :: acc.snd.fst).get ⟨0, zero_lt_length_list⟩).snd f.assignments[↑i] = true ∧
    ∀ (k : Fin (l :: acc.snd.fst).length), k ≠ ⟨0, zero_lt_length_list⟩ → ((l :: acc.snd.fst).get k).fst.val ≠ ↑i