internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : i = k2
⊢ False
Tactic:
next i_eq_k2 =>
have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
by_cases j = k1
. next j_eq_k1 =>
  rw [← j_eq_k1, hj, ← bi_eq_bj, bi_eq_false] at h1
  simp only [Prod.mk.injEq, and_false] at h1
. next j_ne_k1 =>
  specialize h5 j j_ne_k1 j_ne_k2
  rw [hj, li_eq_lj] at h5
  simp (config := { decide := true}) only at h5
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
⊢ False
Tactic:
have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
⊢ False
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
⊢ False
Tactic:
by_cases j = k1
Proof state after:
case pos
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : j = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : j = k1
⊢ False

case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False
Tactic:
. next j_eq_k1 =>
  rw [← j_eq_k1, hj, ← bi_eq_bj, bi_eq_false] at h1
  simp only [Prod.mk.injEq, and_false] at h1
Proof state after:
case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False
Tactic:
. next j_ne_k1 =>
  specialize h5 j j_ne_k1 j_ne_k2
  rw [hj, li_eq_lj] at h5
  simp (config := { decide := true}) only at h5
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
⊢ j ≠ k2
Tactic:
rw [← i_eq_k2]
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
⊢ j ≠ i
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
⊢ j ≠ i
Tactic:
exact i_ne_j.symm
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
case pos
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : j = k1
⊢ False
Tactic:
next j_eq_k1 =>
rw [← j_eq_k1, hj, ← bi_eq_bj, bi_eq_false] at h1
simp only [Prod.mk.injEq, and_false] at h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_eq_k1 : j = k1
⊢ False
Tactic:
rw [← j_eq_k1, hj, ← bi_eq_bj, bi_eq_false] at h1
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (lj, false) = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_eq_k1 : j = k1
⊢ False
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (lj, false) = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_eq_k1 : j = k1
⊢ False
Tactic:
simp only [Prod.mk.injEq, and_false] at h1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
h✝ : ¬j = k1
⊢ False
Tactic:
next j_ne_k1 =>
specialize h5 j j_ne_k1 j_ne_k2
rw [hj, li_eq_lj] at h5
simp (config := { decide := true}) only at h5
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_ne_k1 : ¬j = k1
⊢ False
Tactic:
specialize h5 j j_ne_k1 j_ne_k2
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_ne_k1 : ¬j = k1
h5 : ¬(f.insertRupUnits units).fst.rupUnits[j].fst.val = li.val
⊢ False
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_ne_k1 : ¬j = k1
h5 : ¬(f.insertRupUnits units).fst.rupUnits[j].fst.val = li.val
⊢ False
Tactic:
rw [hj, li_eq_lj] at h5
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_ne_k1 : ¬j = k1
h5 : ¬(lj, bj).fst.val = lj.val
⊢ False
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
bi_eq_false : bi = false
i_eq_k2 : i = k2
j_ne_k2 : j ≠ k2
j_ne_k1 : ¬j = k1
h5 : ¬(lj, bj).fst.val = lj.val
⊢ False
Tactic:
simp (config := { decide := true}) only at h5
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insertRupUnits_nodup
Proof state before:
case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
bi_eq_false : bi = false
h✝ : ¬i = k2
⊢ False
Tactic:
next i_ne_k2 =>
by_cases i = k1
. next i_eq_k1 =>
  rw [← i_eq_k1, hi, bi_eq_false] at h1
  simp only [Prod.mk.injEq, and_false] at h1
. next i_ne_k1 =>
  specialize h5 i i_ne_k1 i_ne_k2
  rw [hi] at h5
  simp only [not_true] at h5
Proof state after:
no goals