From 7a5a08960a30420a9a2524dcab76c331c72c7764 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 10 Sep 2024 16:17:38 +1000 Subject: [PATCH] feat: cleanup of List.findIdx / List.take lemmas (#5293) --- src/Init/Data/List/Find.lean | 23 ++++++++------- src/Init/Data/List/Nat/TakeDrop.lean | 43 +++++++++++++++++++++++++++- src/Init/Data/List/TakeDrop.lean | 6 ++-- 3 files changed, 59 insertions(+), 13 deletions(-) diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index d98de43397..85a3376726 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -539,7 +539,7 @@ theorem findIdx_lt_length {p : α → Bool} {xs : List α} : /-- `p` does not hold for elements with indices less than `xs.findIdx p`. -/ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.findIdx p) : - ¬p (xs[i]'(Nat.le_trans h (findIdx_le_length p))) := by + p (xs[i]'(Nat.le_trans h (findIdx_le_length p))) = false := by revert i induction xs with | nil => intro i h; rw [findIdx_nil] at h; simp at h @@ -547,10 +547,14 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs intro i h have ho := h rw [findIdx_cons] at h - have npx : ¬p x := by intro y; rw [y, cond_true] at h; simp at h + have npx : p x = false := by + apply eq_false_of_ne_true + intro y + rw [y, cond_true] at h + simp at h simp [npx, cond_false] at h cases i.eq_zero_or_pos with - | inl e => simpa only [e, Fin.zero_eta, get_cons_zero] + | inl e => simpa [e, Fin.zero_eta, get_cons_zero] | inr e => have ipm := Nat.succ_pred_eq_of_pos e have ilt := Nat.le_trans ho (findIdx_le_length p) @@ -560,11 +564,11 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs /-- If `¬ p xs[j]` for all `j < i`, then `i ≤ xs.findIdx p`. -/ theorem le_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) - (h2 : ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji h))) : i ≤ xs.findIdx p := by + (h2 : ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false) : i ≤ xs.findIdx p := by apply Decidable.byContradiction intro f simp only [Nat.not_le] at f - exact absurd (@findIdx_getElem _ p xs (Nat.lt_trans f h)) (h2 (xs.findIdx p) f) + exact absurd (@findIdx_getElem _ p xs (Nat.lt_trans f h)) (by simpa using h2 (xs.findIdx p) f) /-- If `¬ p xs[j]` for all `j ≤ i`, then `i < xs.findIdx p`. -/ theorem lt_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) @@ -576,19 +580,18 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs /-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) : - xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji h)) := by + xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by refine ⟨fun f ↦ ⟨f ▸ (@findIdx_getElem _ p xs (f ▸ h)), fun _ hji ↦ not_of_lt_findIdx (f ▸ hji)⟩, - fun ⟨h1, h2⟩ ↦ ?_⟩ + fun ⟨_, h2⟩ ↦ ?_⟩ apply Nat.le_antisymm _ (le_findIdx_of_not h h2) apply Decidable.byContradiction intro h3 simp at h3 - exact not_of_lt_findIdx h3 h1 + simp_all [not_of_lt_findIdx h3] theorem findIdx_append (p : α → Bool) (l₁ l₂ : List α) : (l₁ ++ l₂).findIdx p = - if l₁.findIdx p < l₁.length then l₁.findIdx p else l₂.findIdx p + l₁.length := by - simp + if ∃ x, x ∈ l₁ ∧ p x = true then l₁.findIdx p else l₂.findIdx p + l₁.length := by induction l₁ with | nil => simp | cons x xs ih => diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index bd2440e899..428f839f75 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -6,6 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M prelude import Init.Data.List.Zip import Init.Data.List.Sublist +import Init.Data.List.Find import Init.Data.Nat.Lemmas /-! @@ -268,6 +269,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] @@ -288,7 +309,7 @@ theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n th theorem getLast_drop {l : List α} (h : l.drop n ≠ []) : (l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by - simp only [ne_eq, drop_eq_nil_iff_le] at h + simp only [ne_eq, drop_eq_nil_iff] at h apply Option.some_inj.1 simp only [← getLast?_eq_getLast, getLast?_drop, ite_eq_right_iff] omega @@ -435,6 +456,26 @@ theorem reverse_drop {l : List α} {n : Nat} : rw [w, take_zero, drop_of_length_le, reverse_nil] omega +/-! ### findIdx -/ + +theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs.take (xs.findIdx p)) : + p x = false := by + simp only [mem_take_iff_getElem, forall_exists_index] at h + obtain ⟨i, h, rfl⟩ := h + exact not_of_lt_findIdx (by omega) + +theorem findIdx_take {xs : List α} {n : Nat} {p : α → Bool} : + (xs.take n).findIdx p = min n (xs.findIdx p) := by + induction xs generalizing n with + | nil => simp + | cons x xs ih => + cases n + · simp + · simp only [take_succ_cons, findIdx_cons, ih, cond_eq_if] + split + · simp + · rw [Nat.add_min_add_right] + /-! ### rotateLeft -/ @[simp] theorem rotateLeft_replicate (n) (a : α) : rotateLeft (replicate m a) n = replicate m a := by diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index eee93f1d99..04f7e76a89 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -7,7 +7,7 @@ prelude import Init.Data.List.Lemmas /-! -# Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`. +# Lemmas about `List.take` and `List.drop`. -/ namespace List @@ -129,7 +129,7 @@ theorem drop_tail (l : List α) (n : Nat) : l.tail.drop n = l.drop (n + 1) := by rw [← drop_drop, drop_one] @[simp] -theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by +theorem drop_eq_nil_iff {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by refine ⟨fun h => ?_, drop_eq_nil_of_le⟩ induction k generalizing l with | zero => @@ -141,6 +141,8 @@ theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] ↔ l.length · simp only [drop] at h simpa [Nat.succ_le_succ_iff] using hk h +@[deprecated drop_eq_nil_iff (since := "2024-09-10")] abbrev drop_eq_nil_iff_le := @drop_eq_nil_iff + @[simp] theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ k = 0 ∨ l = [] := by cases l <;> cases k <;> simp [Nat.succ_ne_zero]