internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : i = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : ¬i = k1
⊢ False
Tactic:
. next i_eq_k1 =>
  have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
  by_cases j = k2
  . next j_eq_k2 =>
    rw [← j_eq_k2, hj, bi_eq_true] at h2
    simp at h2
  . next j_ne_k2 =>
    specialize h5 j j_ne_k1 j_ne_k2
    simp (config := { decide := true }) only [hj] at h5
Proof state after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : ¬i = k1
⊢ False
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : ¬i = k1
⊢ False
Tactic:
. next i_ne_k1 =>
  by_cases i = k2
  . next i_eq_k2 =>
    rw [← i_eq_k2, hi, bi_eq_true] at h2
    simp at h2
  . next i_ne_k2 =>
    specialize h5 i i_ne_k1 i_ne_k2
    simp only [hi, not_true] at h5
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
h✝ : i = k1
⊢ False
Tactic:
next i_eq_k1 =>
have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
by_cases j = k2
. next j_eq_k2 =>
  rw [← j_eq_k2, hj, bi_eq_true] at h2
  simp at h2
. next j_ne_k2 =>
  specialize h5 j j_ne_k1 j_ne_k2
  simp (config := { decide := true }) only [hj] at h5
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ False
Tactic:
have j_ne_k1 : j ≠ k1 := by rw [← i_eq_k1]; exact i_ne_j.symm
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
⊢ False
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
⊢ False
Tactic:
by_cases j = k2
Proof state after:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : j = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : j = k2
⊢ False

case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False
Tactic:
. next j_eq_k2 =>
  rw [← j_eq_k2, hj, bi_eq_true] at h2
  simp at h2
Proof state after:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False
Tactic:
. next j_ne_k2 =>
  specialize h5 j j_ne_k1 j_ne_k2
  simp (config := { decide := true }) only [hj] at h5
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ j ≠ k1
Tactic:
rw [← i_eq_k1]
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ j ≠ i
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
⊢ j ≠ i
Tactic:
exact i_ne_j.symm
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
case pos
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : j = k2
⊢ False
Tactic:
next j_eq_k2 =>
rw [← j_eq_k2, hj, bi_eq_true] at h2
simp at h2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_eq_k2 : j = k2
⊢ False
Tactic:
rw [← j_eq_k2, hj, bi_eq_true] at h2
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (li, true) = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_eq_k2 : j = k2
⊢ False
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (li, true) = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_eq_k2 : j = k2
⊢ False
Tactic:
simp at h2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
h✝ : ¬j = k2
⊢ False
Tactic:
next j_ne_k2 =>
specialize h5 j j_ne_k1 j_ne_k2
simp (config := { decide := true }) only [hj] at h5
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRatUnits units).fst.ratUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRatUnits units).fst.ratUnits[k].fst.val = li.val
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_ne_k2 : ¬j = k2
⊢ False
Tactic:
specialize h5 j j_ne_k1 j_ne_k2
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_ne_k2 : ¬j = k2
h5 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False
Theorem: LRAT.DefaultFormula.insertRatUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
i j : Fin (f.insertRatUnits units).fst.ratUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRatUnits units).fst.ratUnits[i] = (li, bi)
hj : (f.insertRatUnits units).fst.ratUnits[j] = (li, bi)
k1 k2 : Fin (f.insertRatUnits units).fst.ratUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRatUnits units).fst.ratUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRatUnits units).fst.ratUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRatUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_true : bi = true
i_eq_k1 : i = k1
j_ne_k1 : j ≠ k1
j_ne_k2 : ¬j = k2
h5 : ¬(f.insertRatUnits units).fst.ratUnits[j].fst.val = li.val
⊢ False
Tactic:
simp (config := { decide := true }) only [hj] at h5
Proof state after:
no goals