internlm/Lean-Github huggingface dataset:
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
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_j_succ : k ≠ ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬↑k = 0
k_val_ne_zero : ↑k ≠ 0
k' : Nat
k_eq_k'_succ : ↑k = k' + 1
⊢ k' + 1 < (l :: acc.snd.fst).length
Tactic:
rw [← k_eq_k'_succ]
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
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_j_succ : k ≠ ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬↑k = 0
k_val_ne_zero : ↑k ≠ 0
k' : Nat
k_eq_k'_succ : ↑k = k' + 1
⊢ ↑k < (l :: acc.snd.fst).length
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
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_j_succ : k ≠ ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬↑k = 0
k_val_ne_zero : ↑k ≠ 0
k' : Nat
k_eq_k'_succ : ↑k = k' + 1
⊢ ↑k < (l :: acc.snd.fst).length
Tactic:
exact k.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_in_bounds : l.fst.val < acc.fst.size
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_j_succ : k ≠ ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬↑k = 0
k' : Nat
k'_succ_in_bounds : k' + 1 < (l :: acc.snd.fst).length
k_eq_succ : k = ⟨k' + 1, k'_succ_in_bounds⟩
⊢ k' < acc.snd.fst.length
Tactic:
simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
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
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_j_succ : k ≠ ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬↑k = 0
k' : Nat
k'_succ_in_bounds : k' + 1 < acc.snd.fst.length + 1
k_eq_succ : k = ⟨k' + 1, k'_succ_in_bounds⟩
⊢ k' < acc.snd.fst.length
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
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_j_succ : k ≠ ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬↑k = 0
k' : Nat
k'_succ_in_bounds : k' + 1 < acc.snd.fst.length + 1
k_eq_succ : k = ⟨k' + 1, k'_succ_in_bounds⟩
⊢ k' < acc.snd.fst.length
Tactic:
exact Nat.lt_of_succ_lt_succ k'_succ_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
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_j_succ : k ≠ ⟨↑j + 1, j_succ_in_bounds⟩
k_ne_zero : ¬↑k = 0
k' : Nat
k'_succ_in_bounds : k' + 1 < (l :: acc.snd.fst).length
k_eq_succ : k = ⟨k' + 1, k'_succ_in_bounds⟩
k'_in_bounds : k' < acc.snd.fst.length
⊢ ⟨k', k'_in_bounds⟩ ≠ j
Tactic:
simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq] at k_ne_j_succ
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
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_zero : ¬↑k = 0
k' : Nat
k'_succ_in_bounds : k' + 1 < (l :: acc.snd.fst).length
k_eq_succ : k = ⟨k' + 1, k'_succ_in_bounds⟩
k'_in_bounds : k' < acc.snd.fst.length
k_ne_j_succ : ¬k' = ↑j
⊢ ⟨k', k'_in_bounds⟩ ≠ j
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
j : Fin acc.snd.fst.length
j_eq_i : (acc.snd.fst.get j).fst.val = ↑i
h1 : acc.fst[↑i] = addAssignment (acc.snd.fst.get j).snd f.assignments[↑i]
h2 : ¬hasAssignment (acc.snd.fst.get j).snd f.assignments[↑i] = true
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j → (acc.snd.fst.get k).fst.val ≠ ↑i
l' : Literal (PosFin n) := acc.snd.fst.get j
zero_in_bounds : 0 < (l :: acc.snd.fst).length
j_succ_in_bounds : ↑j + 1 < (l :: acc.snd.fst).length
l_ne_i : ¬l.fst.val = ↑i
k : Fin (l :: acc.snd.fst).length
k_ne_zero : ¬↑k = 0
k' : Nat
k'_succ_in_bounds : k' + 1 < (l :: acc.snd.fst).length
k_eq_succ : k = ⟨k' + 1, k'_succ_in_bounds⟩
k'_in_bounds : k' < acc.snd.fst.length
k_ne_j_succ : ¬k' = ↑j
⊢ ⟨k', k'_in_bounds⟩ ≠ j
Tactic:
exact Fin.ne_of_val_ne k_ne_j_succ
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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
⊢ ↑j1 + 1 < (l :: acc.snd.fst).length
Tactic:
simp only [List.length_cons, Nat.succ_eq_add_one]
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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
⊢ ↑j1 + 1 < acc.snd.fst.length + 1
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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
⊢ ↑j1 + 1 < acc.snd.fst.length + 1
Tactic:
exact Nat.succ_lt_succ j1.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_in_bounds : l.fst.val < acc.fst.size
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
⊢ ↑j2 + 1 < (l :: acc.snd.fst).length
Tactic:
simp only [List.length_cons, Nat.succ_eq_add_one]
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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
⊢ ↑j2 + 1 < acc.snd.fst.length + 1
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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
⊢ ↑j2 + 1 < acc.snd.fst.length + 1
Tactic:
exact Nat.succ_lt_succ j2.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_in_bounds : l.fst.val < acc.fst.size
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
⊢ l.fst.val ≠ ↑i
Tactic:
intro l_eq_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
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
l_eq_i : l.fst.val = ↑i
⊢ False
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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
l_eq_i : l.fst.val = ↑i
⊢ False
Tactic:
simp only [hasAssignment, Bool.not_eq_true] at h
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
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
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
l_eq_i : l.fst.val = ↑i
h : (if l.snd = true then hasPosAssignment else hasNegAssignment) acc.fst[l.fst.val]! = false
⊢ False