diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index b81cb23c4c..18a043a36c 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1391,16 +1391,22 @@ theorem get_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by simp [getElem_append_right, h, h', h''] -theorem getElem?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : +theorem getElem?_append_left {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : (l₁ ++ l₂)[n]? = l₁[n]? := by have hn' : n < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <| length_append .. ▸ Nat.le_add_right .. simp_all [getElem?_eq_getElem, getElem_append] -@[deprecated (since := "2024-06-12")] +@[deprecated getElem?_append_left (since := "2024-06-12")] theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : (l₁ ++ l₂).get? n = l₁.get? n := by - simp [getElem?_append hn] + simp [getElem?_append_left hn] + +theorem getElem?_append {l₁ l₂ : List α} {n : Nat} : + (l₁ ++ l₂)[n]? = if n < l₁.length then l₁[n]? else l₂[n - l₁.length]? := by + split <;> rename_i h + · exact getElem?_append_left h + · exact getElem?_append_right (by simpa using h) @[simp] theorem head_append_of_ne_nil {l : List α} (w : l ≠ []) : head (l ++ l') (by simp_all) = head l w := by @@ -1868,25 +1874,36 @@ theorem bind_replicate {β} (f : α → List β) : (replicate n a).bind f = (rep | [] => simp | x :: xs => simp +@[simp] theorem reverse_ne_nil_iff {xs : List α} : xs.reverse ≠ [] ↔ xs ≠ [] := + not_congr reverse_eq_nil_iff + theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l → l.reverse[i]? = l[j]? | [], _, _, _ => rfl | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, getElem?_append_right, Nat.succ.injEq] | a::l, i, j+1, h => by have := Nat.succ.inj h; simp at this ⊢ - rw [getElem?_append, getElem?_reverse' _ _ this] + rw [getElem?_append_left, getElem?_reverse' _ _ this] rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _) @[deprecated getElem?_reverse' (since := "2024-06-12")] theorem get?_reverse' {l : List α} (i j) (h : i + j + 1 = length l) : get? l.reverse i = get? l j := by simp [getElem?_reverse' _ _ h] +@[simp] theorem getElem?_reverse {l : List α} {i} (h : i < length l) : l.reverse[i]? = l[l.length - 1 - i]? := getElem?_reverse' _ _ <| by rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h), Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)] +@[simp] +theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) : + l.reverse[i] = l[l.length - 1 - i]'(Nat.sub_one_sub_lt_of_lt (by simpa using h)) := by + apply Option.some.inj + rw [← getElem?_eq_getElem, ← getElem?_eq_getElem] + rw [getElem?_reverse (by simpa using h)] + @[deprecated getElem?_reverse (since := "2024-06-12")] theorem get?_reverse {l : List α} {i} (h : i < length l) : get? l.reverse i = get? l (l.length - 1 - i) := by @@ -2144,6 +2161,14 @@ theorem dropLast_cons_of_ne_nil {α : Type u} {x : α} {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: l.dropLast := by simp [dropLast, h] +theorem dropLast_concat_getLast : ∀ {l : List α} (h : l ≠ []), dropLast l ++ [getLast l h] = l + | [], h => absurd rfl h + | [a], h => rfl + | a :: b :: l, h => by + rw [dropLast_cons₂, cons_append, getLast_cons (cons_ne_nil _ _)] + congr + exact dropLast_concat_getLast (cons_ne_nil b l) + @[simp] theorem map_dropLast (f : α → β) (l : List α) : l.dropLast.map f = (l.map f).dropLast := by induction l with | nil => rfl diff --git a/src/Init/Data/List/Nat.lean b/src/Init/Data/List/Nat.lean index 55c81b0bf0..877061671f 100644 --- a/src/Init/Data/List/Nat.lean +++ b/src/Init/Data/List/Nat.lean @@ -7,4 +7,5 @@ prelude import Init.Data.List.Nat.Basic import Init.Data.List.Nat.Pairwise import Init.Data.List.Nat.Range +import Init.Data.List.Nat.Sublist import Init.Data.List.Nat.TakeDrop diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index 38b37018d4..849f2a8cdc 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -25,6 +25,14 @@ theorem length_filter_lt_length_iff_exists (l) : simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using countP_pos (fun x => ¬p x) (l := l) +/-! ### reverse -/ + +theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) : + l[i] = l.reverse[l.length - 1 - i]'(by simpa using Nat.sub_one_sub_lt_of_lt h) := by + rw [getElem_reverse] + congr + omega + /-! ### leftpad -/ /-- The length of the List returned by `List.leftpad n a l` is equal diff --git a/src/Init/Data/List/Nat/Sublist.lean b/src/Init/Data/List/Nat/Sublist.lean new file mode 100644 index 0000000000..a371c0584c --- /dev/null +++ b/src/Init/Data/List/Nat/Sublist.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +prelude +import Init.Data.List.Sublist +import Init.Data.List.Nat.Basic +import Init.Data.List.Nat.TakeDrop +import Init.Data.Nat.Lemmas + +/-! +# Further lemmas about `List.IsSuffix` / `List.IsPrefix` / `List.IsInfix`. + +These are in a separate file from most of the lemmas about `List.IsSuffix` +as they required importing more lemmas about natural numbers, and use `omega`. +-/ + +namespace List + +theorem IsSuffix.getElem {x y : List α} (h : x <:+ y) {n} (hn : n < x.length) : + x[n] = y[y.length - x.length + n]'(by have := h.length_le; omega) := by + rw [getElem_eq_getElem_reverse, h.reverse.getElem, getElem_reverse] + congr + have := h.length_le + omega + +theorem isSuffix_iff : l₁ <:+ l₂ ↔ + l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] := by + suffices l₁.length ≤ l₂.length ∧ l₁ <:+ l₂ ↔ + l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] by + constructor + · intro h + exact this.mp ⟨h.length_le, h⟩ + · intro h + exact (this.mpr h).2 + simp only [and_congr_right_iff] + intro le + rw [← reverse_prefix, isPrefix_iff] + simp only [length_reverse] + constructor + · intro w i h + specialize w (l₁.length - 1 - i) (by omega) + rw [getElem?_reverse (by omega)] at w + have p : l₂.length - 1 - (l₁.length - 1 - i) = i + l₂.length - l₁.length := by omega + rw [p] at w + rw [w, getElem_reverse] + congr + omega + · intro w i h + rw [getElem?_reverse] + specialize w (l₁.length - 1 - i) (by omega) + have p : l₁.length - 1 - i + l₂.length - l₁.length = l₂.length - 1 - i := by omega + rw [p] at w + rw [w, getElem_reverse] + exact Nat.lt_of_lt_of_le h le + +theorem isInfix_iff : l₁ <:+: l₂ ↔ + ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + k]? = some l₁[i] := by + constructor + · intro h + obtain ⟨t, p, s⟩ := infix_iff_suffix_prefix.mp h + refine ⟨t.length - l₁.length, by have := p.length_le; have := s.length_le; omega, ?_⟩ + rw [isSuffix_iff] at p + obtain ⟨p', p⟩ := p + rw [isPrefix_iff] at s + intro i h + rw [s _ (by omega)] + specialize p i (by omega) + rw [Nat.add_sub_assoc (by omega)] at p + rw [← getElem?_eq_getElem, p] + · rintro ⟨k, le, w⟩ + refine ⟨l₂.take k, l₂.drop (k + l₁.length), ?_⟩ + ext1 i + rw [getElem?_append] + split + · rw [getElem?_append] + split + · rw [getElem?_take]; simp_all; omega + · simp_all + have p : i = (i - k) + k := by omega + rw [p, w _ (by omega), getElem?_eq_getElem] + · congr 2 + omega + · omega + · rw [getElem?_drop] + congr + simp_all + omega + +theorem suffix_iff_eq_append : l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂ := + ⟨by rintro ⟨r, rfl⟩; simp only [length_append, Nat.add_sub_cancel_right, take_left], fun e => + ⟨_, e⟩⟩ + +theorem prefix_take_iff {x y : List α} {n : Nat} : x <+: y.take n ↔ x <+: y ∧ x.length ≤ n := by + constructor + · intro h + constructor + · exact List.IsPrefix.trans h <| List.take_prefix n y + · replace h := h.length_le + rw [length_take, Nat.le_min] at h + exact h.left + · intro ⟨hp, hl⟩ + have hl' := hp.length_le + rw [List.prefix_iff_eq_take] at * + rw [hp, List.take_take] + simp [Nat.min_eq_left, hl, hl'] + +theorem suffix_iff_eq_drop : l₁ <:+ l₂ ↔ l₁ = drop (length l₂ - length l₁) l₂ := + ⟨fun h => append_cancel_left <| (suffix_iff_eq_append.1 h).trans (take_append_drop _ _).symm, + fun e => e.symm ▸ drop_suffix _ _⟩ + +theorem prefix_take_le_iff {L : List α} (hm : m < L.length) : + L.take m <+: L.take n ↔ m ≤ n := by + simp only [prefix_iff_eq_take, length_take] + induction m generalizing L n with + | zero => simp [Nat.min_eq_left, eq_self_iff_true, Nat.zero_le, take] + | succ m IH => + cases L with + | nil => simp_all + | cons l ls => + cases n with + | zero => + simp + | succ n => + simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm + simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm] + +end List diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean index 06bc757620..4a0da8468c 100644 --- a/src/Init/Data/List/Nat/TakeDrop.lean +++ b/src/Init/Data/List/Nat/TakeDrop.lean @@ -5,6 +5,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.Nat.Lemmas /-! @@ -199,6 +200,19 @@ theorem map_eq_append_split {f : α → β} {l : List α} {s₁ s₂ : List β} rw [← length_map l f, h, length_append] apply Nat.le_add_right +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, 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 + +theorem take_sublist_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l <+ take n l := + (take_prefix_take_left l h).sublist + +theorem take_subset_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l ⊆ take n l := + (take_sublist_take_left l h).subset + /-! ### drop -/ theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length := by @@ -319,7 +333,7 @@ theorem set_eq_take_append_cons_drop {l : List α} {n : Nat} {a : α} : split <;> rename_i h · ext1 m by_cases h' : m < n - · rw [getElem?_append (by simp [length_take]; omega), getElem?_set_ne (by omega), + · rw [getElem?_append_left (by simp [length_take]; omega), getElem?_set_ne (by omega), getElem?_take h'] · by_cases h'' : m = n · subst h'' diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 63a0974599..3d4dc28d45 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -1,7 +1,8 @@ /- Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro +Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, + Kim Morrison -/ prelude import Init.Data.List.TakeDrop @@ -84,6 +85,8 @@ theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a @[simp] theorem subset_nil {l : List α} : l ⊆ [] ↔ l = [] := ⟨fun h => match l with | [] => rfl | _::_ => (nomatch h (.head ..)), fun | rfl => Subset.refl _⟩ +theorem eq_nil_of_subset_nil {l : List α} : l ⊆ [] → l = [] := subset_nil.mp + theorem map_subset {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ := fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _) @@ -192,6 +195,9 @@ theorem mem_of_cons_sublist {a : α} {l₁ l₂ : List α} (s : a :: l₁ <+ l @[simp] theorem sublist_nil {l : List α} : l <+ [] ↔ l = [] := ⟨fun s => subset_nil.1 s.subset, fun H => H ▸ Sublist.refl _⟩ +theorem eq_nil_of_sublist_nil {l : List α} (s : l <+ []) : l = [] := + eq_nil_of_subset_nil <| s.subset + theorem Sublist.length_le : l₁ <+ l₂ → length l₁ ≤ length l₂ | .slnil => Nat.le_refl 0 | .cons _l s => le_succ_of_le (length_le s) @@ -208,6 +214,18 @@ theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l theorem Sublist.length_eq (s : l₁ <+ l₂) : length l₁ = length l₂ ↔ l₁ = l₂ := ⟨s.eq_of_length, congrArg _⟩ +theorem tail_sublist : ∀ l : List α, tail l <+ l + | [] => .slnil + | a::l => sublist_cons_self a l + +protected theorem Sublist.tail : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → tail l₁ <+ tail l₂ + | _, _, slnil => .slnil + | _, _, Sublist.cons _ h => (tail_sublist _).trans h + | _, _, Sublist.cons₂ _ h => h + +theorem Sublist.of_cons_cons {l₁ l₂ : List α} {a b : α} (h : a :: l₁ <+ b :: l₂) : l₁ <+ l₂ := + h.tail + protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂ := by induction s with | slnil => simp @@ -512,6 +530,10 @@ theorem join_sublist_iff {L : List (List α)} {l} : instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) := decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist +protected theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ n, l₁.drop n <+ l₂.drop n + | _, _, h, 0 => h + | _, _, h, n + 1 => by rw [← drop_tail, ← drop_tail]; exact h.tail.drop n + /-! ### IsPrefix / IsSuffix / IsInfix -/ @[simp] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩ @@ -527,17 +549,17 @@ theorem IsPrefix.isInfix : l₁ <+: l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => theorem IsSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨t, [], by rw [h, append_nil]⟩ -@[simp] theorem nil_prefix (l : List α) : [] <+: l := ⟨l, rfl⟩ +@[simp] theorem nil_prefix {l : List α} : [] <+: l := ⟨l, rfl⟩ -@[simp] theorem nil_suffix (l : List α) : [] <:+ l := ⟨l, append_nil _⟩ +@[simp] theorem nil_suffix {l : List α} : [] <:+ l := ⟨l, append_nil _⟩ -@[simp] theorem nil_infix (l : List α) : [] <:+: l := (nil_prefix _).isInfix +@[simp] theorem nil_infix {l : List α} : [] <:+: l := nil_prefix.isInfix -@[simp] theorem prefix_refl (l : List α) : l <+: l := ⟨[], append_nil _⟩ +@[simp] theorem prefix_refl {l : List α} : l <+: l := ⟨[], append_nil _⟩ -@[simp] theorem suffix_refl (l : List α) : l <:+ l := ⟨[], rfl⟩ +@[simp] theorem suffix_refl {l : List α} : l <:+ l := ⟨[], rfl⟩ -@[simp] theorem infix_refl (l : List α) : l <:+: l := (prefix_refl l).isInfix +@[simp] theorem infix_refl {l : List α} : l <:+: l := prefix_refl.isInfix @[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a] @@ -573,6 +595,50 @@ protected theorem IsSuffix.sublist (h : l₁ <:+ l₂) : l₁ <+ l₂ := protected theorem IsSuffix.subset (hl : l₁ <:+ l₂) : l₁ ⊆ l₂ := hl.sublist.subset +@[simp] theorem infix_nil : l <:+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ infix_refl)⟩ + +@[simp] theorem prefix_nil : l <+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ prefix_refl)⟩ + +@[simp] theorem suffix_nil : l <:+ [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ suffix_refl)⟩ + +theorem eq_nil_of_infix_nil (h : l <:+: []) : l = [] := infix_nil.mp h +theorem eq_nil_of_prefix_nil (h : l <+: []) : l = [] := prefix_nil.mp h +theorem eq_nil_of_suffix_nil (h : l <:+ []) : l = [] := suffix_nil.mp h + +theorem IsPrefix.ne_nil {x y : List α} (h : x <+: y) (hx : x ≠ []) : y ≠ [] := by + rintro rfl; exact hx <| List.prefix_nil.mp h + +theorem IsSuffix.ne_nil {x y : List α} (h : x <:+ y) (hx : x ≠ []) : y ≠ [] := by + rintro rfl; exact hx <| List.suffix_nil.mp h + +theorem IsInfix.ne_nil {x y : List α} (h : x <:+: y) (hx : x ≠ []) : y ≠ [] := by + rintro rfl; exact hx <| List.infix_nil.mp h + +theorem IsInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length := + h.sublist.length_le + +theorem IsPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length := + h.sublist.length_le + +theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length := + h.sublist.length_le + +theorem IsPrefix.getElem {x y : List α} (h : x <+: y) {n} (hn : n < x.length) : + x[n] = y[n]'(Nat.le_trans hn h.length_le) := by + obtain ⟨_, rfl⟩ := h + exact (List.getElem_append n hn).symm + +-- See `Init.Data.List.Nat.Sublist` for `IsSuffix.getElem`. + +theorem IsPrefix.mem (hx : a ∈ l₁) (hl : l₁ <+: l₂) : a ∈ l₂ := + hl.subset hx + +theorem IsSuffix.mem (hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂ := + hl.subset hx + +theorem IsInfix.mem (hx : a ∈ l₁) (hl : l₁ <:+: l₂) : a ∈ l₂ := + hl.subset hx + @[simp] theorem reverse_suffix : reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂ := ⟨fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]⟩, fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_append, e]⟩⟩ @@ -586,25 +652,35 @@ protected theorem IsSuffix.subset (hl : l₁ <:+ l₂) : l₁ ⊆ l₂ := reverse_reverse] · rw [append_assoc, ← reverse_append, ← reverse_append, e] -theorem IsInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length := - h.sublist.length_le +theorem IsInfix.reverse : l₁ <:+: l₂ → reverse l₁ <:+: reverse l₂ := + reverse_infix.2 -theorem IsPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length := - h.sublist.length_le +theorem IsSuffix.reverse : l₁ <:+ l₂ → reverse l₁ <+: reverse l₂ := + reverse_prefix.2 -theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length := - h.sublist.length_le +theorem IsPrefix.reverse : l₁ <+: l₂ → reverse l₁ <:+ reverse l₂ := + reverse_suffix.2 -@[simp] theorem infix_nil : l <:+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ infix_refl _)⟩ +theorem IsPrefix.head {x y : List α} (h : x <+: y) (hx : x ≠ []) : + x.head hx = y.head (h.ne_nil hx) := by + cases x <;> cases y <;> simp only [head_cons, ne_eq, not_true_eq_false] at hx ⊢ + all_goals (obtain ⟨_, h⟩ := h; injection h) -@[simp] theorem prefix_nil : l <+: [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ prefix_refl _)⟩ +theorem IsSuffix.getLast {x y : List α} (h : x <:+ y) (hx : x ≠ []) : + x.getLast hx = y.getLast (h.ne_nil hx) := by + rw [← head_reverse (by simpa), h.reverse.head, + head_reverse (by rintro h; simp only [reverse_eq_nil_iff] at h; simp_all)] -@[simp] theorem suffix_nil : l <:+ [] ↔ l = [] := ⟨(sublist_nil.1 ·.sublist), (· ▸ suffix_refl _)⟩ +theorem prefix_concat (a : α) (l) : l <+: concat l a := by simp -theorem infix_iff_prefix_suffix (l₁ l₂ : List α) : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ := +theorem infix_iff_prefix_suffix {l₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ := ⟨fun ⟨_, t, e⟩ => ⟨l₁ ++ t, ⟨_, rfl⟩, e ▸ append_assoc .. ▸ ⟨_, rfl⟩⟩, fun ⟨_, ⟨t, rfl⟩, s, e⟩ => ⟨s, t, append_assoc .. ▸ e⟩⟩ +theorem infix_iff_suffix_prefix {l₁ l₂ : List α} : l₁ <:+: l₂ ↔ ∃ t, l₁ <:+ t ∧ t <+: l₂ := + ⟨fun ⟨s, t, e⟩ => ⟨s ++ l₁, ⟨_, rfl⟩, ⟨t, e⟩⟩, + fun ⟨_, ⟨s, rfl⟩, t, e⟩ => ⟨s, t, append_assoc .. ▸ e⟩⟩ + theorem IsInfix.eq_of_length (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂ := h.sublist.eq_of_length @@ -616,7 +692,7 @@ theorem IsSuffix.eq_of_length (h : l₁ <:+ l₂) : l₁.length = l₂.length theorem prefix_of_prefix_length_le : ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂ - | [], l₂, _, _, _, _ => nil_prefix _ + | [], l₂, _, _, _, _ => nil_prefix | a :: l₁, b :: l₂, _, ⟨r₁, rfl⟩, ⟨r₂, e⟩, ll => by injection e with _ e'; subst b rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩ (le_of_succ_le_succ ll) with ⟨r₃, rfl⟩ @@ -679,6 +755,41 @@ theorem infix_cons_iff : l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+ · exact h.isInfix · exact infix_cons hl₁ +theorem prefix_concat_iff {l₁ l₂ : List α} {a : α} : + l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂ := by + simp only [← concat_eq_append, ← reverse_suffix, reverse_concat, suffix_cons_iff] + simp only [concat_eq_append, ← reverse_concat, reverse_eq_iff, reverse_reverse] + +theorem suffix_concat_iff {l₁ l₂ : List α} {a : α} : + l₁ <:+ l₂ ++ [a] ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂ := by + rw [← reverse_prefix, ← concat_eq_append, reverse_concat, prefix_cons_iff] + simp only [reverse_eq_nil_iff] + apply or_congr_right + constructor + · rintro ⟨t, w, h⟩ + exact ⟨t.reverse, by simpa using congrArg reverse w, by simpa using h.reverse⟩ + · rintro ⟨t, rfl, h⟩ + exact ⟨t.reverse, by simp, by simpa using h.reverse⟩ + +theorem infix_concat_iff {l₁ l₂ : List α} {a : α} : + l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂ := by + rw [← reverse_infix, ← concat_eq_append, reverse_concat, infix_cons_iff, reverse_infix, + ← reverse_prefix, reverse_concat] + +theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? = some l₁[i] := by + induction l₁ generalizing l₂ with + | nil => simp + | cons a l₁ ih => + cases l₂ with + | nil => + simpa using ⟨0, by simp⟩ + | cons b l₂ => + simp only [cons_append, cons_prefix_cons, ih] + rw (config := {occs := .pos [2]}) [← Nat.and_forall_add_one] + simp [Nat.succ_lt_succ_iff, eq_comm] + +-- See `Init.Data.List.Nat.Sublist` for `isSuffix_iff` and `ifInfix_iff`. + theorem infix_of_mem_join : ∀ {L : List (List α)}, l ∈ L → l <:+: join L | l' :: _, h => match h with @@ -717,6 +828,60 @@ theorem mem_of_mem_take {l : List α} (h : a ∈ l.take n) : a ∈ l := theorem mem_of_mem_drop {n} {l : List α} (h : a ∈ l.drop n) : a ∈ l := drop_subset _ _ h +theorem drop_suffix_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l <:+ drop m l := by + rw [← Nat.sub_add_cancel h, ← drop_drop] + apply drop_suffix + +-- See `Init.Data.List.Nat.TakeDrop` for `take_prefix_take_left`. + +theorem drop_sublist_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l <+ drop m l := + (drop_suffix_drop_left l h).sublist + +theorem drop_subset_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l ⊆ drop m l := + (drop_sublist_drop_left l h).subset + +theorem takeWhile_prefix (p : α → Bool) : l.takeWhile p <+: l := + ⟨l.dropWhile p, takeWhile_append_dropWhile p l⟩ + +theorem dropWhile_suffix (p : α → Bool) : l.dropWhile p <:+ l := + ⟨l.takeWhile p, takeWhile_append_dropWhile p l⟩ + +theorem takeWhile_sublist (p : α → Bool) : l.takeWhile p <+ l := + (takeWhile_prefix p).sublist + +theorem dropWhile_sublist (p : α → Bool) : l.dropWhile p <+ l := + (dropWhile_suffix p).sublist + +theorem takeWhile_subset {l : List α} (p : α → Bool) : l.takeWhile p ⊆ l := + (takeWhile_sublist p).subset + +theorem dropWhile_subset {l : List α} (p : α → Bool) : l.dropWhile p ⊆ l := + (dropWhile_sublist p).subset + +theorem dropLast_prefix : ∀ l : List α, l.dropLast <+: l + | [] => ⟨nil, by rw [dropLast, List.append_nil]⟩ + | a :: l => ⟨_, dropLast_concat_getLast (cons_ne_nil a l)⟩ + +theorem dropLast_sublist (l : List α) : l.dropLast <+ l := + (dropLast_prefix l).sublist + +theorem dropLast_subset (l : List α) : l.dropLast ⊆ l := + (dropLast_sublist l).subset + +theorem tail_suffix (l : List α) : tail l <:+ l := by rw [← drop_one]; apply drop_suffix + +theorem IsPrefix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.map f <+: l₂.map f := by + obtain ⟨r, rfl⟩ := h + rw [map_append]; apply prefix_append + +theorem IsSuffix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f := by + obtain ⟨r, rfl⟩ := h + rw [map_append]; apply suffix_append + +theorem IsInfix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f := by + obtain ⟨r₁, r₂, rfl⟩ := h + rw [map_append, map_append]; apply infix_append + theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.filter p <+: l₂.filter p := by obtain ⟨xs, rfl⟩ := h @@ -732,6 +897,21 @@ theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ obtain ⟨xs, ys, rfl⟩ := h rw [filter_append, filter_append]; apply infix_append _ +theorem IsPrefix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : + filterMap f l₁ <+: filterMap f l₂ := by + obtain ⟨xs, rfl⟩ := h + rw [filterMap_append]; apply prefix_append + +theorem IsSuffix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : + filterMap f l₁ <:+ filterMap f l₂ := by + obtain ⟨xs, rfl⟩ := h + rw [filterMap_append]; apply suffix_append + +theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : + filterMap f l₁ <:+: filterMap f l₂ := by + obtain ⟨xs, ys, rfl⟩ := h + rw [filterMap_append, filterMap_append]; apply infix_append + @[simp] theorem isPrefixOf_iff_prefix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.isPrefixOf l₂ ↔ l₁ <+: l₂ := by induction l₁ generalizing l₂ with @@ -751,4 +931,13 @@ instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+: l₂) := instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+ l₂) := decidable_of_iff (l₁.isSuffixOf l₂) isSuffixOf_iff_suffix +theorem prefix_iff_eq_append : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ := + ⟨by rintro ⟨r, rfl⟩; rw [drop_left], fun e => ⟨_, e⟩⟩ + +theorem prefix_iff_eq_take : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ := + ⟨fun h => append_cancel_right <| (prefix_iff_eq_append.1 h).trans (take_append_drop _ _).symm, + fun e => e.symm ▸ take_prefix _ _⟩ + +-- See `Init.Data.List.Nat.Sublist` for `suffix_iff_eq_append`, `prefix_take_iff`, and `suffix_iff_eq_drop`. + end List diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 6f4fd0df1f..621fcf5f9c 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -94,6 +94,25 @@ theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l. theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := getElem?_take (Nat.lt_succ_self n) +@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l + | m, [] => by simp + | 0, l => by simp + | m + 1, a :: l => + calc + drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl + _ = drop (n + m) l := drop_drop n m l + _ = drop (n + (m + 1)) (a :: l) := rfl + +theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l) + | 0, _, _ => by simp + | _, _, [] => by simp + | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop .. + +@[deprecated drop_drop (since := "2024-06-15")] +theorem drop_add (m n) (l : List α) : drop (m + n) l = drop m (drop n l) := by + simp [drop_drop] + +@[simp] theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := by induction l generalizing n with | nil => simp @@ -102,6 +121,10 @@ theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := · simp · simp [hl] +@[simp] +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 refine' ⟨fun h => _, drop_eq_nil_of_le⟩ @@ -226,24 +249,6 @@ theorem dropLast_eq_take (l : List α) : l.dropLast = l.take (l.length - 1) := b dsimp rw [map_drop f t] -@[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l - | m, [] => by simp - | 0, l => by simp - | m + 1, a :: l => - calc - drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl - _ = drop (n + m) l := drop_drop n m l - _ = drop (n + (m + 1)) (a :: l) := rfl - -theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l) - | 0, _, _ => by simp - | _, _, [] => by simp - | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop .. - -@[deprecated drop_drop (since := "2024-06-15")] -theorem drop_add (m n) (l : List α) : drop (m + n) l = drop m (drop n l) := by - simp [drop_drop] - /-! ### takeWhile and dropWhile -/ theorem takeWhile_cons (p : α → Bool) (a : α) (l : List α) : diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index ccb9d9a84f..01a12c9dde 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -1087,6 +1087,10 @@ protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a = protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h] +protected theorem sub_one_sub_lt_of_lt (h : a < b) : b - 1 - a < b := by + rw [← Nat.sub_add_eq] + exact sub_lt (zero_lt_of_lt h) (Nat.lt_add_right a Nat.one_pos) + /-! ## Mul sub distrib -/ theorem pred_mul (n m : Nat) : pred n * m = n * m - m := by