From 180c1cef08a870a247fc4dd06dd25b0e8e69657f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 10 Sep 2024 16:04:49 +1000 Subject: [PATCH] chore: switch primes on List.getElem_take fix fix --- src/Init/Data/List/Nat/Range.lean | 2 +- src/Init/Data/List/Nat/TakeDrop.lean | 36 +++++++++++++++++++++------- 2 files changed, 29 insertions(+), 9 deletions(-) diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean index 959db5dc48e4..c8d1d62d5299 100644 --- a/src/Init/Data/List/Nat/Range.lean +++ b/src/Init/Data/List/Nat/Range.lean @@ -176,7 +176,7 @@ theorem pairwise_le_range (n : Nat) : Pairwise (· ≤ ·) (range n) := theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by apply List.ext_getElem · simp - · simp (config := { contextual := true }) [← getElem_take, Nat.lt_min] + · simp (config := { contextual := true }) [getElem_take, Nat.lt_min] theorem nodup_range (n : Nat) : Nodup (range n) := by simp (config := {decide := true}) only [range_eq_range', nodup_range'] diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index bd2440e89913..951f70eea53b 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -35,23 +35,23 @@ theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by sim /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the big list to the small list. -/ -theorem getElem_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) : +theorem getElem_take' (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) : L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) := getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append .. /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the small list to the big list. -/ -theorem getElem_take' (L : List α) {j i : Nat} {h : i < (L.take j).length} : +theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} : (L.take j)[i] = L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by - rw [length_take, Nat.lt_min] at h; rw [getElem_take L _ h.1] + rw [length_take, Nat.lt_min] at h; rw [getElem_take' L _ h.1] /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the big list to the small list. -/ -@[deprecated getElem_take (since := "2024-06-12")] +@[deprecated getElem_take' (since := "2024-06-12")] theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) : get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by - simp [getElem_take _ hi hj] + simp [getElem_take' _ hi hj] /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the small list to the big list. -/ @@ -59,7 +59,7 @@ length `> i`. Version designed to rewrite from the small list to the big list. - theorem get_take' (L : List α) {j i} : get (L.take j) i = get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by - simp [getElem_take'] + simp [getElem_take] theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) : (l.take n)[m]? = none := @@ -109,7 +109,7 @@ theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none e theorem getLast_take {l : List α} (h : l.take n ≠ []) : (l.take n).getLast h = l[n - 1]?.getD (l.getLast (by simp_all)) := by - rw [getLast_eq_getElem, getElem_take'] + rw [getLast_eq_getElem, getElem_take] simp [length_take, Nat.min_def] simp at h split @@ -203,7 +203,7 @@ theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β} theorem take_prefix_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l <+: take n l := by rw [isPrefix_iff] intro i w - rw [getElem?_take_of_lt, getElem_take', getElem?_eq_getElem] + rw [getElem?_take_of_lt, getElem_take, getElem?_eq_getElem] simp only [length_take] at w exact Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le w (Nat.min_le_left _ _)) h @@ -268,6 +268,26 @@ theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by simp +theorem mem_take_iff_getElem {l : List α} {a : α} : + a ∈ l.take n ↔ ∃ (i : Nat) (hm : i < min n l.length), l[i] = a := by + rw [mem_iff_getElem] + constructor + · rintro ⟨i, hm, rfl⟩ + simp at hm + refine ⟨i, by omega, by rw [getElem_take]⟩ + · rintro ⟨i, hm, rfl⟩ + refine ⟨i, by simpa, by rw [getElem_take]⟩ + +theorem mem_drop_iff_getElem {l : List α} {a : α} : + a ∈ l.drop n ↔ ∃ (i : Nat) (hm : i + n < l.length), l[n + i] = a := by + rw [mem_iff_getElem] + constructor + · rintro ⟨i, hm, rfl⟩ + simp at hm + refine ⟨i, by omega, by rw [getElem_drop]⟩ + · rintro ⟨i, hm, rfl⟩ + refine ⟨i, by simp; omega, by rw [getElem_drop]⟩ + theorem head?_drop (l : List α) (n : Nat) : (l.drop n).head? = l[n]? := by rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]