max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: restore @[simp] on List.getElem_mem et al (#5520)

Browse source
This commit is contained in:
Kim Morrison 2024-09-29 23:28:13 +10:00 • committed by GitHub
parent 3a46fd0fde
commit 7d26a1604f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Data/List/Lemmas.lean
View file

@ -489,7 +489,7 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
| _ :: _, 0, _ => .head ..
| _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
@ -1018,7 +1018,7 @@ theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
simp [getLast!, getLast_eq_getLastD]
theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
@[simp] theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
| [], h => absurd rfl h
| [_], _ => .head ..
| _::a::l, _ => .tail _ <| getLast_mem (cons_ne_nil a l)
@ -1116,7 +1116,7 @@ theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys
@[simp] theorem head?_isSome : l.head?.isSome ↔ l ≠ [] := by
cases l <;> simp
theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
@[simp] theorem head_mem : ∀ {l : List α} (h : l ≠ []), head l h ∈ l
| [], h => absurd rfl h
| _::_, _ => .head ..