internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.left
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ derivedLits_arr[⟨↑j2, j2_lt_derivedLits_arr_size⟩] = (⟨↑i, ⋯⟩, false)
Tactic:
simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get, ← j2_eq_i]
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.left
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ derivedLits.get ⟨↑j2, ⋯⟩ = (⟨(derivedLits.get j2).fst.val, ⋯⟩, false)
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.left
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ derivedLits.get ⟨↑j2, ⋯⟩ = (⟨(derivedLits.get j2).fst.val, ⋯⟩, false)
Tactic:
rw [← j2_eq_false]
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.left
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ derivedLits.get ⟨↑j2, ⋯⟩ = (⟨(derivedLits.get j2).fst.val, ⋯⟩, (derivedLits.get j2).snd)
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.left
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ derivedLits.get ⟨↑j2, ⋯⟩ = (⟨(derivedLits.get j2).fst.val, ⋯⟩, (derivedLits.get j2).snd)
Tactic:
rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ f'.assignments[↑i] = both ∧
    f.assignments[↑i] = unassigned ∧
      ∀ (k : Fin derivedLits_arr.size),
        ↑k ≥ 0 →
          k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩ →
            k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩ → derivedLits_arr[k].fst.val ≠ ↑i
Tactic:
apply And.intro h1 ∘ And.intro h2
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ ∀ (k : Fin derivedLits_arr.size),
    ↑k ≥ 0 →
      k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩ → k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩ → derivedLits_arr[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ ∀ (k : Fin derivedLits_arr.size),
    ↑k ≥ 0 →
      k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩ → k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩ → derivedLits_arr[k].fst.val ≠ ↑i
Tactic:
intro k _ k_ne_j1 k_ne_j2
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1 : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2 : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
⊢ derivedLits_arr[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1 : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2 : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
⊢ derivedLits_arr[k].fst.val ≠ ↑i
Tactic:
have k_in_bounds : k < derivedLits.length := by
  have k_property := k.2
  simp only [derivedLits_arr_def, Array.size_mk] at k_property
  exact k_property
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1 : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2 : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
k_in_bounds : ↑k < derivedLits.length
⊢ derivedLits_arr[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1 : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2 : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
k_in_bounds : ↑k < derivedLits.length
⊢ derivedLits_arr[k].fst.val ≠ ↑i
Tactic:
have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by
  apply Fin.ne_of_val_ne
  simp only
  exact Fin.val_ne_of_ne k_ne_j1
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1✝ : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2 : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
k_in_bounds : ↑k < derivedLits.length
k_ne_j1 : ⟨↑k, k_in_bounds⟩ ≠ j1
⊢ derivedLits_arr[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1✝ : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2 : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
k_in_bounds : ↑k < derivedLits.length
k_ne_j1 : ⟨↑k, k_in_bounds⟩ ≠ j1
⊢ derivedLits_arr[k].fst.val ≠ ↑i
Tactic:
have k_ne_j2 : ⟨k.1, k_in_bounds⟩ ≠ j2 := by
  apply Fin.ne_of_val_ne
  simp only
  exact Fin.val_ne_of_ne k_ne_j2
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1✝ : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2✝ : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
k_in_bounds : ↑k < derivedLits.length
k_ne_j1 : ⟨↑k, k_in_bounds⟩ ≠ j1
k_ne_j2 : ⟨↑k, k_in_bounds⟩ ≠ j2
⊢ derivedLits_arr[k].fst.val ≠ ↑i
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1✝ : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2✝ : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
k_in_bounds : ↑k < derivedLits.length
k_ne_j1 : ⟨↑k, k_in_bounds⟩ ≠ j1
k_ne_j2 : ⟨↑k, k_in_bounds⟩ ≠ j2
⊢ derivedLits_arr[k].fst.val ≠ ↑i
Tactic:
simp only [Fin.getElem_fin, Array.getElem_eq_data_get, ne_eq, derivedLits_arr_def]
Proof state after:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1✝ : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2✝ : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
k_in_bounds : ↑k < derivedLits.length
k_ne_j1 : ⟨↑k, k_in_bounds⟩ ≠ j1
k_ne_j2 : ⟨↑k, k_in_bounds⟩ ≠ j2
⊢ ¬(derivedLits.get ⟨↑k, ⋯⟩).fst.val = ↑i
Theorem: LRAT.DefaultFormula.restoreAssignments_performRupCheck_base_case
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
k : Fin derivedLits_arr.size
a✝ : ↑k ≥ 0
k_ne_j1✝ : k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩
k_ne_j2✝ : k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩
k_in_bounds : ↑k < derivedLits.length
k_ne_j1 : ⟨↑k, k_in_bounds⟩ ≠ j1
k_ne_j2 : ⟨↑k, k_in_bounds⟩ ≠ j2
⊢ ¬(derivedLits.get ⟨↑k, ⋯⟩).fst.val = ↑i
Tactic:
exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
Proof state after:
no goals