internlm/Lean-Github huggingface dataset:
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type ?u.18089
τ : Type ?u.18088
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
⊢ size (update cont i f) = size cont
Tactic:
rw [size_update]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
⊢ ↑i ≠ ↑j → get (update cont i f) j = get cont (Fin.cast ⋯ j)
Tactic:
intro h
Proof state after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ get (update cont i f) j = get cont (Fin.cast ⋯ j)
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ get (update cont i f) j = get cont (Fin.cast ⋯ j)
Tactic:
conv => lhs; rw [get_def]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ get (toList (update cont i f)) (Fin.cast ⋯ j) = get cont (Fin.cast ⋯ j)
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ get (toList (update cont i f)) (Fin.cast ⋯ j) = get cont (Fin.cast ⋯ j)
Tactic:
simp [List.instSeqList]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ (toList (update cont i f)).get (Fin.cast ⋯ j) = get cont (Fin.cast ⋯ j)
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ (toList (update cont i f)).get (Fin.cast ⋯ j) = get cont (Fin.cast ⋯ j)
Tactic:
rw [List.get_eq_get _ _ _ _ ?list_eq ?idx_eq]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ?m.18568.get ?m.18570 = get cont (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ List τ

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ Fin ?m.18568.length

case list_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ toList (update cont i f) = ?m.18568

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.18570
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ toList (update cont i f) = ?m.18568
Tactic:
case list_eq =>
    apply toList_update
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ (update (toList cont) (Fin.cast ⋯ i) f).get ?m.18570 = get cont (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ Fin (update (toList cont) (Fin.cast ⋯ i) f).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.18570
Tactic:
simp [List.instSeqList]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).get ?m.18570 = get cont (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ Fin (update (toList cont) (Fin.cast ⋯ i) f).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.18570
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).get ?m.18570 = get cont (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ Fin (update (toList cont) (Fin.cast ⋯ i) f).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.18570
Tactic:
rw [List.get_set_ne _ _ _ ?h]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get cont (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ℕ

case h
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑i ≠ ?m.18745

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨?m.18745, ?h⟩
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get cont (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ℕ

case h
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑i ≠ ?m.18745

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨?m.18745, ?h⟩
Tactic:
conv => rhs; rw [get_def]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get (toList cont) (Fin.cast ⋯ (Fin.cast ⋯ j))

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ℕ

case h
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑i ≠ ?m.18745

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨?m.18745, ?h⟩
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get (toList cont) (Fin.cast ⋯ (Fin.cast ⋯ j))

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ℕ

case h
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑i ≠ ?m.18745

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨?m.18745, ?h⟩
Tactic:
rfl
Proof state after:
case h
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑i ≠ ↑(Fin.cast ⋯ j)

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑(Fin.cast ⋯ j), ?h⟩
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length
Tactic:
case h => simpa [size_def, List.instSeqList] using j.isLt
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑(Fin.cast ⋯ j), ⋯⟩
Tactic:
case idx_eq => simp
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑i ≠ ↑(Fin.cast ⋯ j)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ toList (update cont i f) = ?m.18568
Tactic:
apply toList_update
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length
Tactic:
simpa [size_def, List.instSeqList] using j.isLt
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_ne
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑(Fin.cast ⋯ j), ⋯⟩
Tactic:
simp
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
⊢ get (update cont i f) j = if ↑i = ↑j then f (get cont (Fin.cast ⋯ j)) else get cont (Fin.cast ⋯ j)
Tactic:
rcases i with ⟨i,hi⟩
Proof state after:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : Fin (size (update cont ⟨i, hi⟩ f))
⊢ get (update cont ⟨i, hi⟩ f) j = if ↑⟨i, hi⟩ = ↑j then f (get cont (Fin.cast ⋯ j)) else get cont (Fin.cast ⋯ j)
Theorem: LeanColls.Seq.get_update
Proof state before:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : Fin (size (update cont ⟨i, hi⟩ f))
⊢ get (update cont ⟨i, hi⟩ f) j = if ↑⟨i, hi⟩ = ↑j then f (get cont (Fin.cast ⋯ j)) else get cont (Fin.cast ⋯ j)
Tactic:
rcases j with ⟨j,hj⟩
Proof state after:
case mk.mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : ℕ
hj : j < size (update cont ⟨i, hi⟩ f)
⊢ get (update cont ⟨i, hi⟩ f) ⟨j, hj⟩ =
    if ↑⟨i, hi⟩ = ↑⟨j, hj⟩ then f (get cont (Fin.cast ⋯ ⟨j, hj⟩)) else get cont (Fin.cast ⋯ ⟨j, hj⟩)
Theorem: LeanColls.Seq.get_update
Proof state before:
case mk.mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : ℕ
hj : j < size (update cont ⟨i, hi⟩ f)
⊢ get (update cont ⟨i, hi⟩ f) ⟨j, hj⟩ =
    if ↑⟨i, hi⟩ = ↑⟨j, hj⟩ then f (get cont (Fin.cast ⋯ ⟨j, hj⟩)) else get cont (Fin.cast ⋯ ⟨j, hj⟩)
Tactic:
by_cases i = j <;> simp [*]
Proof state after:
no goals
Theorem: LeanColls.BitVec.shiftLeft_bitwiseOr
Proof state before:
a b i : ℕ
⊢ (a ||| b) >>> i = a >>> i ||| b >>> i
Tactic:
sorry
Proof state after:
no goals
Theorem: LeanColls.BitVec.shiftRight_shiftLeft
Proof state before:
i j : ℕ
⊢ 2 ^ i >>> j = if j > i then 0 else 2 ^ (i - j)
Tactic:
sorry
Proof state after:
no goals
Theorem: LeanColls.BitVec.get_set
Proof state before:
n : ℕ
bv : BitVec n
i : Fin n
x : Bool
j : Fin n
⊢ (bv.set i x).get j = if i = j then x else bv.get j
Tactic:
simp [get, set]
Proof state after:
n : ℕ
bv : BitVec n
i : Fin n
x : Bool
j : Fin n
⊢ ((Seq.get
            (if x = true then { data := sorryAx ByteArray true, hsize := ⋯ }
              else { data := sorryAx ByteArray true, hsize := ⋯ }).data
            ⟨↑j / 8, ⋯⟩).land
        (UInt8.shiftLeft 1 (↑j % 8).toUInt8) !=
      0) =
    if i = j then x else (Seq.get bv.data ⟨↑j / 8, ⋯⟩).land (UInt8.shiftLeft 1 (↑j % 8).toUInt8) != 0
Theorem: LeanColls.BitVec.zero_shiftRight
Proof state before:
i : ℕ
⊢ 0 >>> i = 0
Tactic:
induction i <;> simp [shiftRight_zero, shiftRight_succ]
Proof state after:
no goals
Theorem: LeanColls.BitVec.get_empty
Proof state before:
n : ℕ
i : Fin n
⊢ (empty n).get i = false
Tactic:
match i with
| ⟨i,h_i⟩ =>
simp [empty,get]
Proof state after:
no goals
Theorem: LeanColls.BitVec.get_empty
Proof state before:
n : ℕ
i✝ : Fin n
i : ℕ
h_i : i < n
⊢ (empty n).get ⟨i, h_i⟩ = false
Tactic:
simp [empty,get]
Proof state after:
n : ℕ
i✝ : Fin n
i : ℕ
h_i : i < n
⊢ (Seq.get (sorryAx ByteArray true) ⟨i / 8, ⋯⟩).land (UInt8.shiftLeft 1 (i % 8).toUInt8) = 0
Theorem: LeanColls.Indexed.get_set_eq
Proof state before:
C : Type u_2
ι : Type u_3
τ : Type u_1
inst✝¹ : Indexed C ι τ
inst✝ : LawfulIndexed C ι τ
i : ι
a : τ
cont : C
⊢ get (set cont i a) i = a
Tactic:
simp only [LawfulIndexed.get_set_eq]
Proof state after:
no goals
Theorem: LeanColls.Indexed.get_set
Proof state before:
C : Type u_3
ι : Type u_1
τ : Type u_2
inst✝² : Indexed C ι τ
inst✝¹ : LawfulIndexed C ι τ
inst✝ : DecidableEq ι
cont : C
i j : ι
a : τ
⊢ get (set cont i a) j = if i = j then a else get cont j
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: LeanColls.Indexed.get_update_eq
Proof state before:
C : Type u_2
ι : Type u_3
τ : Type u_1
inst✝¹ : Indexed C ι τ
inst✝ : LawfulIndexed C ι τ
i : ι
f : τ → τ
cont : C
⊢ get (update cont i f) i = f (get cont i)
Tactic:
simp [LawfulIndexed.get_update_eq]
Proof state after:
no goals
Theorem: LeanColls.Indexed.get_update
Proof state before:
C : Type u_3
ι : Type u_1
τ : Type u_2
inst✝² : Indexed C ι τ
inst✝¹ : LawfulIndexed C ι τ
inst✝ : DecidableEq ι
cont : C
i j : ι
f : τ → τ
⊢ get (update cont i f) j = if i = j then f (get cont j) else get cont j
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: LeanColls.Range.mem_def
Proof state before:
x : ℕ
r : Range
⊢ x ∈ r ↔ r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
Tactic:
simp [Membership.mem, contains]
Proof state after:
x : ℕ
r : Range
⊢ (r.start ≤ x ∧ x < r.stop) ∧ r.step ∣ x - r.start ↔ r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
Theorem: LeanColls.Range.mem_def
Proof state before:
x : ℕ
r : Range
⊢ (r.start ≤ x ∧ x < r.stop) ∧ r.step ∣ x - r.start ↔ r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
Tactic:
exact and_assoc
Proof state after:
no goals
Theorem: LeanColls.Range.nth_ge_start
Proof state before:
r : Range
i : ℕ
⊢ r.nth i ≥ r.start
Tactic:
simp [nth]
Proof state after:
no goals
Theorem: LeanColls.Range.nth_sub_start
Proof state before:
r : Range
i : ℕ
⊢ r.step ∣ r.nth i - r.start
Tactic:
simp [nth]
Proof state after:
no goals
Theorem: LeanColls.Range.ofNth_nth
Proof state before:
r : Range
i : ℕ
⊢ r.ofNth (r.nth i) = i
Tactic:
simp [nth, ofNth]
Proof state after:
no goals
Theorem: LeanColls.Range.nth_ofNth
Proof state before:
r : Range
x : ℕ
h : x ∈ r
⊢ r.nth (r.ofNth x) = x
Tactic:
simp [mem_def] at h
Proof state after:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.nth (r.ofNth x) = x
Theorem: LeanColls.Range.nth_ofNth
Proof state before:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.nth (r.ofNth x) = x
Tactic:
simp [nth, ofNth]
Proof state after:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) / r.step * r.step = x
Theorem: LeanColls.Range.nth_ofNth
Proof state before:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) / r.step * r.step = x
Tactic:
rw [Nat.div_mul_cancel h.2.2]
Proof state after:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) = x
Theorem: LeanColls.Range.nth_ofNth
Proof state before:
r : Range
x : ℕ
h : r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
⊢ r.start + (x - r.start) = x
Tactic:
simp only [*, ge_iff_le, add_tsub_cancel_of_le]
Proof state after:
no goals
Theorem: LeanColls.Range.nth_lt_stop_iff_lt_size
Proof state before:
r : Range
i : ℕ
⊢ r.nth i < r.stop ↔ i < r.size
Tactic:
simp [nth, size, Nat.lt_iff_add_one_le,
      Nat.le_div_iff_mul_le r.step_pos]
Proof state after:
r : Range
i : ℕ
⊢ r.start + i * r.step + 1 ≤ r.stop ↔ (i + 1) * r.step ≤ r.stop - r.start + r.step - 1
Theorem: LeanColls.Range.nth_lt_stop_iff_lt_size
Proof state before:
r : Range
i : ℕ
⊢ r.start + i * r.step + 1 ≤ r.stop ↔ (i + 1) * r.step ≤ r.stop - r.start + r.step - 1
Tactic:
zify
Proof state after:
r : Range
i : ℕ
⊢ ↑r.start + ↑i * ↑r.step + 1 ≤ ↑r.stop ↔ (↑i + 1) * ↑r.step ≤ ↑(r.stop - r.start + r.step - 1)
Theorem: LeanColls.Range.nth_lt_stop_iff_lt_size
Proof state before:
r : Range
i : ℕ
⊢ ↑r.start + ↑i * ↑r.step + 1 ≤ ↑r.stop ↔ (↑i + 1) * ↑r.step ≤ ↑(r.stop - r.start + r.step - 1)
Tactic:
simp
Proof state after:
r : Range
i : ℕ
⊢ ↑r.start + ↑i * ↑r.step + 1 ≤ ↑r.stop ↔ (↑i + 1) * ↑r.step ≤ ↑r.stop - ↑r.start + ↑r.step - 1
Theorem: LeanColls.Range.nth_lt_stop_iff_lt_size
Proof state before:
r : Range
i : ℕ
⊢ ↑r.start + ↑i * ↑r.step + 1 ≤ ↑r.stop ↔ (↑i + 1) * ↑r.step ≤ ↑r.stop - ↑r.start + ↑r.step - 1
Tactic:
constructor <;> intro h <;> linarith
Proof state after:
no goals
Theorem: LeanColls.Range.nth_mem_iff_lt_size
Proof state before:
r : Range
i : ℕ
⊢ r.nth i ∈ r ↔ i < r.size
Tactic:
simp [mem_def, nth_lt_stop_iff_lt_size]
Proof state after:
no goals
Theorem: LeanColls.Range.nth_size_eq_stop
Proof state before:
r : Range
h : r.step = 1
⊢ r.nth r.size = r.stop
Tactic:
simp [nth, size, h]
Proof state after:
no goals
Theorem: LeanColls.Range.nth_size_lt
Proof state before:
r : Range
⊢ r.nth r.size < r.stop + r.step
Tactic:
simp [nth, size]
Proof state after:
r : Range
⊢ r.start + (r.stop - r.start + r.step - 1) / r.step * r.step < r.stop + r.step
Theorem: LeanColls.Range.nth_size_lt
Proof state before:
r : Range
⊢ r.start + (r.stop - r.start + r.step - 1) / r.step * r.step < r.stop + r.step
Tactic:
rw [Nat.add_comm, Nat.lt_iff_add_one_le, Nat.add_assoc]
Proof state after:
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step + (r.start + 1) ≤ r.stop + r.step
Theorem: LeanColls.Range.nth_size_lt
Proof state before:
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step + (r.start + 1) ≤ r.stop + r.step
Tactic:
apply Nat.add_le_of_le_sub
Proof state after:
case hle
r : Range
⊢ r.start + 1 ≤ r.stop + r.step

case h
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step ≤ r.stop + r.step - (r.start + 1)
Theorem: LeanColls.Range.nth_size_lt
Proof state before:
case h
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step ≤ r.stop + r.step - (r.start + 1)
Tactic:
convert Nat.div_mul_le_self _ _ using 1
Proof state after:
case h.e'_4
r : Range
⊢ r.stop + r.step - (r.start + 1) = r.stop - r.start + r.step - 1
Theorem: LeanColls.Range.nth_size_lt
Proof state before:
case h.e'_4
r : Range
⊢ r.stop + r.step - (r.start + 1) = r.stop - r.start + r.step - 1
Tactic:
rw [Nat.add_comm, Nat.sub_add_eq,
    Nat.add_sub_assoc r.start_le_stop,
    Nat.add_comm,
    Nat.add_sub_assoc r.step_pos]
Proof state after:
no goals
Theorem: LeanColls.Range.nth_size_lt
Proof state before:
case hle
r : Range
⊢ r.start + 1 ≤ r.stop + r.step
Tactic:
apply Nat.add_le_add
Proof state after:
case hle.h₁
r : Range
⊢ r.start ≤ r.stop

case hle.h₂
r : Range
⊢ 1 ≤ r.step
Theorem: LeanColls.Range.nth_size_lt
Proof state before:
case hle.h₁
r : Range
⊢ r.start ≤ r.stop

case hle.h₂
r : Range
⊢ 1 ≤ r.step
Tactic:
simp
Proof state after:
case hle.h₂
r : Range
⊢ 1 ≤ r.step
Theorem: LeanColls.Range.nth_size_lt
Proof state before:
case hle.h₂
r : Range
⊢ 1 ≤ r.step
Tactic:
apply r.step_pos
Proof state after:
no goals
Theorem: LeanColls.Range.size_eq_zero_iff_isEmpty
Proof state before:
r : Range
⊢ r.size = 0 ↔ r.isEmpty = true
Tactic:
simp [size, isEmpty]
Proof state after:
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step = 0 ↔ r.start = r.stop
Theorem: LeanColls.Range.size_eq_zero_iff_isEmpty
Proof state before:
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step = 0 ↔ r.start = r.stop
Tactic:
rw [Nat.div_eq_zero_iff r.step_pos,
    Nat.lt_iff_add_one_le,
    Nat.sub_add_cancel]
Proof state after:
r : Range
⊢ r.stop - r.start + r.step ≤ r.step ↔ r.start = r.stop

r : Range
⊢ 1 ≤ r.stop - r.start + r.step
Theorem: LeanColls.Range.size_eq_zero_iff_isEmpty
Proof state before:
r : Range
⊢ r.stop - r.start + r.step ≤ r.step ↔ r.start = r.stop
Tactic:
simp
Proof state after:
r : Range
⊢ r.stop - r.start = 0 ↔ r.start = r.stop
Theorem: LeanColls.Range.size_eq_zero_iff_isEmpty
Proof state before:
r : Range
⊢ r.stop - r.start = 0 ↔ r.start = r.stop
Tactic:
rw [Nat.sub_eq_zero_iff_le, Nat.le_antisymm_iff]
Proof state after:
r : Range
⊢ r.stop ≤ r.start ↔ r.start ≤ r.stop ∧ r.stop ≤ r.start
Theorem: LeanColls.Range.size_eq_zero_iff_isEmpty
Proof state before:
r : Range
⊢ r.stop ≤ r.start ↔ r.start ≤ r.stop ∧ r.stop ≤ r.start
Tactic:
simp only [start_le_stop, true_and]
Proof state after:
no goals
Theorem: LeanColls.Range.size_eq_zero_iff_isEmpty
Proof state before:
r : Range
⊢ 1 ≤ r.stop - r.start + r.step
Tactic:
exact le_add_left r.step_pos
Proof state after:
no goals
Theorem: LeanColls.Range.get_mem
Proof state before:
r : Range
i : Fin r.size
⊢ r.get i ∈ r
Tactic:
rcases i with ⟨i,hi⟩
Proof state after:
case mk
r : Range
i : ℕ
hi : i < r.size
⊢ r.get ⟨i, hi⟩ ∈ r
Theorem: LeanColls.Range.get_mem
Proof state before:
case mk
r : Range
i : ℕ
hi : i < r.size
⊢ r.get ⟨i, hi⟩ ∈ r
Tactic:
simp [get, mem_def, nth_lt_stop_iff_lt_size]
Proof state after:
case mk
r : Range
i : ℕ
hi : i < r.size
⊢ i < r.size