internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
i_eq_k1 : ⟨↑i, i_in_bounds⟩ = ⟨↑j, j_in_bounds⟩
j_eq_k1 : ⟨↑j, j_in_bounds⟩ = k1
⊢ False
Tactic:
simp only [Fin.mk.injEq] at i_eq_k1
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
j_eq_k1 : ⟨↑j, j_in_bounds⟩ = k1
i_eq_k1 : ↑i = ↑j
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
j_eq_k1 : ⟨↑j, j_in_bounds⟩ = k1
i_eq_k1 : ↑i = ↑j
⊢ False
Tactic:
exact i_ne_j (Fin.eq_of_val_eq i_eq_k1)
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
h✝ : ¬⟨↑i, i_in_bounds⟩ = k1
⊢ False
Tactic:
next i_ne_k1 =>
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_data_get, ne_eq, derivedLits_arr_def, li] at h3
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
i_ne_k1 : ¬⟨↑i, i_in_bounds⟩ = k1
⊢ False
Tactic:
specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
i_ne_k1 : ¬⟨↑i, i_in_bounds⟩ = k1
h3 : (derivedLits.get ⟨↑i, i_in_bounds⟩).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
li_eq_true : li.snd = true
i_ne_k2 : ⟨↑i, i_in_bounds⟩ ≠ k2
j_ne_k2 : ⟨↑j, j_in_bounds⟩ ≠ k2
i_ne_k1 : ¬⟨↑i, i_in_bounds⟩ = k1
h3 : (derivedLits.get ⟨↑i, i_in_bounds⟩).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
⊢ False
Tactic:
simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_data_get, ne_eq, derivedLits_arr_def, li] at h3
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
h✝ : ¬li.snd = true
⊢ False
Tactic:
next li_eq_false =>
simp only [Bool.not_eq_true] at li_eq_false
have i_ne_k1 : ⟨i.1, i_in_bounds⟩ ≠ k1 := by
  intro i_eq_k1
  rw [← i_eq_k1] at k1_eq_true
  simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get, k1_eq_true, li] at li_eq_false
have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
  intro j_eq_k1
  rw [← j_eq_k1] at k1_eq_true
  simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get] at li_eq_lj
  simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get, k1_eq_true, li_eq_lj, li] at li_eq_false
by_cases ⟨i.1, i_in_bounds⟩ = k2
. next i_eq_k2 =>
  have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
    intro j_eq_k2
    rw [← j_eq_k2] at i_eq_k2
    simp only [Fin.mk.injEq] at i_eq_k2
    exact i_ne_j (Fin.eq_of_val_eq i_eq_k2)
  specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
  simp only [li, li_eq_lj, derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get, ne_eq, not_true] at h3
. next i_ne_k2 =>
  specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
  simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_data_get, ne_eq, derivedLits_arr_def, li] at h3
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_false : ¬li.snd = true
⊢ False
Tactic:
simp only [Bool.not_eq_true] at li_eq_false
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_false : li.snd = false
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_false : li.snd = false
⊢ False
Tactic:
have i_ne_k1 : ⟨i.1, i_in_bounds⟩ ≠ k1 := by
  intro i_eq_k1
  rw [← i_eq_k1] at k1_eq_true
  simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get, k1_eq_true, li] at li_eq_false
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_false : li.snd = false
i_ne_k1 : ⟨↑i, i_in_bounds⟩ ≠ k1
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_false : li.snd = false
i_ne_k1 : ⟨↑i, i_in_bounds⟩ ≠ k1
⊢ False
Tactic:
have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
  intro j_eq_k1
  rw [← j_eq_k1] at k1_eq_true
  simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get] at li_eq_lj
  simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_data_get, k1_eq_true, li_eq_lj, li] at li_eq_false
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_false : li.snd = false
i_ne_k1 : ⟨↑i, i_in_bounds⟩ ≠ k1
j_ne_k1 : ⟨↑j, j_in_bounds⟩ ≠ k1
⊢ False
Theorem: LRAT.DefaultFormula.derivedLits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
i_in_bounds : ↑i < derivedLits.length
j_in_bounds : ↑j < derivedLits.length
k1 k2 : Fin derivedLits.length
left✝³ : (derivedLits.get k1).fst.val = ↑⟨li.fst.val, ⋯⟩
left✝² : (derivedLits.get k2).fst.val = ↑⟨li.fst.val, ⋯⟩
k1_eq_true : (derivedLits.get k1).snd = true
k2_eq_false : (derivedLits.get k2).snd = false
left✝¹ : (f.performRupCheck rupHints).fst.assignments[↑⟨li.fst.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨li.fst.val, ⋯⟩] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ k1 → k ≠ k2 → (derivedLits.get k).fst.val ≠ ↑⟨li.fst.val, ⋯⟩
li_eq_false : li.snd = false
i_ne_k1 : ⟨↑i, i_in_bounds⟩ ≠ k1
j_ne_k1 : ⟨↑j, j_in_bounds⟩ ≠ k1
h✝ : ¬⟨↑i, i_in_bounds⟩ = k2
⊢ False
Tactic:
. next i_ne_k2 =>
  specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
  simp (config := { decide := true }) only [Fin.getElem_fin, Array.getElem_eq_data_get, ne_eq, derivedLits_arr_def, li] at h3
Proof state after:
no goals