From fff845d879adf43e1865b58da9402dca43cac6c7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 18 Jun 2024 14:55:49 +1000 Subject: [PATCH] chore: @[simp] List.getElem?_eq_getElem --- src/Init/Data/List/Lemmas.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 4df5eeb5e6d6..b3a7f9ec8e8b 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -154,7 +154,7 @@ theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none | _ :: l, _+1, h => by rw [getElem?_cons_succ, getElem?_len_le (l := l) <| Nat.le_of_succ_le_succ h] -theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by +@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem] theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by @@ -245,9 +245,12 @@ theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂) (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ := ext_getElem hl (by simp_all) -@[simp] theorem getElem?_concat_length : ∀ (l : List α) (a : α), (l ++ [a])[l.length]? = some a - | [], a => rfl - | b :: l, a => by rw [cons_append, length_cons]; simp [getElem?_concat_length] +@[simp] theorem getElem_concat_length : ∀ (l : List α) (a : α) (i) (_ : i = l.length) (w), (l ++ [a])[i]'w = a + | [], a, _, h, _ => by subst h; simp + | _ :: l, a, _, h, _ => by simp [getElem_concat_length, h] + +theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? = some a := by + simp @[deprecated getElem?_concat_length (since := "2024-06-12")] theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp