From 45af92fcd1846d7ec61125ab0fbd939f38ca68fe Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 16 Sep 2024 19:25:24 +1000 Subject: [PATCH] feat: lemmas about List.tail (#5360) --- src/Init/Data/List/Attach.lean | 52 +++++++++++++++++---------- src/Init/Data/List/Count.lean | 14 ++++++++ src/Init/Data/List/Lemmas.lean | 60 +++++++++++++++++++++++++++++++ src/Init/Data/List/Nat/Basic.lean | 20 +++++++++++ src/Init/Data/List/Nat/Count.lean | 55 ++++++++++++++++++++++++++++ src/Init/Data/List/Nat/Range.lean | 6 ++++ src/Init/Data/List/Range.lean | 16 ++++++++- src/Init/Data/List/Zip.lean | 17 ++++++++- 8 files changed, 220 insertions(+), 20 deletions(-) diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean index 0a3b83f0ba..7b8dc11a60 100644 --- a/src/Init/Data/List/Attach.lean +++ b/src/Init/Data/List/Attach.lean @@ -130,24 +130,6 @@ theorem attachWith_map_subtype_val {p : α → Prop} (l : List α) (H : ∀ a (l.attachWith p H).map Subtype.val = l := (attachWith_map_coe _ _ _).trans (List.map_id _) -theorem countP_attach (l : List α) (p : α → Bool) : - l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by - simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val] - -theorem countP_attachWith {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (q : α → Bool) : - (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by - simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val] - -@[simp] -theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) : - l.attach.count a = l.count ↑a := - Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _ - -@[simp] -theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (a : {x // p x}) : - (l.attachWith p H).count a = l.count ↑a := - Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _ - @[simp] theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach | ⟨a, h⟩ => by @@ -312,6 +294,20 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) : | nil => simp at h | cons x xs => simp [head_attach, h] +@[simp] theorem tail_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α) + (H : ∀ (a : α), a ∈ xs → P a) : + (xs.pmap f H).tail = xs.tail.pmap f (fun a h => H a (mem_of_mem_tail h)) := by + cases xs <;> simp + +@[simp] theorem tail_attachWith {P : α → Prop} {xs : List α} + {H : ∀ (a : α), a ∈ xs → P a} : + (xs.attachWith P H).tail = xs.tail.attachWith P (fun a h => H a (mem_of_mem_tail h)) := by + cases xs <;> simp + +@[simp] theorem tail_attach (xs : List α) : + xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by + cases xs <;> simp + theorem attach_map {l : List α} (f : α → β) : (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by induction l <;> simp [*] @@ -492,4 +488,24 @@ theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) : xs.attach.getLast h = ⟨xs.getLast (by simpa using h), getLast_mem (by simpa using h)⟩ := by simp only [getLast_eq_head_reverse, reverse_attach, head_map, head_attach] +@[simp] +theorem countP_attach (l : List α) (p : α → Bool) : + l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by + simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val] + +@[simp] +theorem countP_attachWith {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (q : α → Bool) : + (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by + simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val] + +@[simp] +theorem count_attach [DecidableEq α] (l : List α) (a : {x // x ∈ l}) : + l.attach.count a = l.count ↑a := + Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _ + +@[simp] +theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (a : {x // p x}) : + (l.attachWith p H).count a = l.count ↑a := + Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attachWith _ _ _ + end List diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index 444f22476f..7f32b071a7 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -115,6 +115,13 @@ theorem IsPrefix.countP_le (s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂ theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le _ theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le _ +-- See `Init.Data.List.Nat.Count` for `Sublist.le_countP : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁`. + +theorem countP_tail_le (l) : countP p l.tail ≤ countP p l := + (tail_sublist l).countP_le _ + +-- See `Init.Data.List.Nat.Count` for `le_countP_tail : countP p l - 1 ≤ countP p l.tail`. + theorem countP_filter (l : List α) : countP p (filter q l) = countP (fun a => p a && q a) l := by simp only [countP_eq_length_filter, filter_filter] @@ -207,6 +214,13 @@ theorem IsPrefix.count_le (h : l₁ <+: l₂) (a : α) : count a l₁ ≤ count theorem IsSuffix.count_le (h : l₁ <:+ l₂) (a : α) : count a l₁ ≤ count a l₂ := h.sublist.count_le _ theorem IsInfix.count_le (h : l₁ <:+: l₂) (a : α) : count a l₁ ≤ count a l₂ := h.sublist.count_le _ +-- See `Init.Data.List.Nat.Count` for `Sublist.le_count : count a l₂ - (l₂.length - l₁.length) ≤ countP a l₁`. + +theorem count_tail_le (a : α) (l) : count a l.tail ≤ count a l := + (tail_sublist l).count_le _ + +-- See `Init.Data.List.Nat.Count` for `le_count_tail : count a l - 1 ≤ count a l.tail`. + theorem count_le_count_cons (a b : α) (l : List α) : count a l ≤ count a (b :: l) := (sublist_cons_self _ _).count_le _ diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 1598ae582d..a8b22562dd 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1045,6 +1045,11 @@ theorem head?_eq_getElem? : ∀ l : List α, head? l = l[0]? | [] => rfl | a :: l => by simp +theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos.mpr h) := by + cases l with + | nil => simp at h + | cons _ _ => simp + theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by cases xs with | nil => simp at h @@ -1105,6 +1110,55 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t theorem mem_of_mem_tail {a : α} {l : List α} (h : a ∈ tail l) : a ∈ l := by induction l <;> simp_all +theorem ne_nil_of_tail_ne_nil {l : List α} : l.tail ≠ [] → l ≠ [] := by + cases l <;> simp + +@[simp] theorem getElem_tail (l : List α) (i : Nat) (h : i < l.tail.length) : + (tail l)[i] = l[i + 1]'(add_lt_of_lt_sub (by simpa using h)) := by + cases l with + | nil => simp at h + | cons _ l => simp + +@[simp] theorem getElem?_tail (l : List α) (i : Nat) : + (tail l)[i]? = l[i + 1]? := by + cases l <;> simp + +@[simp] theorem set_tail (l : List α) (i : Nat) (a : α) : + l.tail.set i a = (l.set (i + 1) a).tail := by + cases l <;> simp + +theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail ≠ []) : 1 < l.length := by + cases l with + | nil => simp at h + | cons _ l => + simp only [tail_cons, ne_eq] at h + exact Nat.lt_add_of_pos_left (length_pos.mpr h) + +@[simp] theorem head_tail (l : List α) (h : l.tail ≠ []) : + (tail l).head h = l[1]'(one_lt_length_of_tail_ne_nil h) := by + cases l with + | nil => simp at h + | cons _ l => simp [head_eq_getElem] + +@[simp] theorem head?_tail (l : List α) : (tail l).head? = l[1]? := by + simp [head?_eq_getElem?] + +@[simp] theorem getLast_tail (l : List α) (h : l.tail ≠ []) : + (tail l).getLast h = l.getLast (ne_nil_of_tail_ne_nil h) := by + simp only [getLast_eq_getElem, length_tail, getElem_tail] + congr + match l with + | _ :: _ :: l => simp + +theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then none else l.getLast? := by + match l with + | [] => simp + | [a] => simp + | _ :: _ :: l => + simp only [tail_cons, length_cons, getLast?_cons_cons] + rw [if_neg] + rintro ⟨⟩ + /-! ## Basic operations -/ /-! ### map -/ @@ -2847,6 +2901,12 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast ( dropLast (a :: replicate n a) = replicate n a := by rw [← replicate_succ, dropLast_replicate, Nat.add_sub_cancel] +@[simp] theorem tail_reverse (l : List α) : l.reverse.tail = l.dropLast.reverse := by + apply ext_getElem + · simp + · intro i h₁ h₂ + simp [Nat.add_comm i, Nat.sub_add_eq] + /-! ### splitAt diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index 4e2f97faf6..5aa05f4dab 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -18,6 +18,26 @@ open Nat namespace List +/-! ### dropLast -/ + +theorem tail_dropLast (l : List α) : tail (dropLast l) = dropLast (tail l) := by + ext1 + simp only [getElem?_tail, getElem?_dropLast, length_tail] + split <;> split + · rfl + · omega + · omega + · rfl + +@[simp] theorem dropLast_reverse (l : List α) : l.reverse.dropLast = l.tail.reverse := by + apply ext_getElem + · simp + · intro i h₁ h₂ + simp only [getElem_dropLast, getElem_reverse, length_tail, getElem_tail] + congr + simp only [length_dropLast, length_reverse, length_tail] at h₁ h₂ + omega + /-! ### filter -/ theorem length_filter_lt_length_iff_exists {l} : diff --git a/src/Init/Data/List/Nat/Count.lean b/src/Init/Data/List/Nat/Count.lean index 4ac93bdce2..a5a3ebe284 100644 --- a/src/Init/Data/List/Nat/Count.lean +++ b/src/Init/Data/List/Nat/Count.lean @@ -28,4 +28,59 @@ theorem count_set [BEq α] (a b : α) (l : List α) (i : Nat) (h : i < l.length) (l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0) := by simp [count_eq_countP, countP_set, h] +/-- +The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list, +minus the difference in the lengths. +-/ +theorem Sublist.le_countP (s : l₁ <+ l₂) (p) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ := by + match s with + | .slnil => simp + | .cons a s => + rename_i l + simp only [countP_cons, length_cons] + have := s.le_countP p + have := s.length_le + split <;> omega + | .cons₂ a s => + rename_i l₁ l₂ + simp only [countP_cons, length_cons] + have := s.le_countP p + have := s.length_le + split <;> omega + +theorem IsPrefix.le_countP (s : l₁ <+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ := + s.sublist.le_countP _ + +theorem IsSuffix.le_countP (s : l₁ <:+ l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ := + s.sublist.le_countP _ + +theorem IsInfix.le_countP (s : l₁ <:+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ := + s.sublist.le_countP _ + +/-- +The number of elements satisfying a predicate in the tail of a list is +at least one less than the number of elements satisfying the predicate in the list. +-/ +theorem le_countP_tail (l) : countP p l - 1 ≤ countP p l.tail := by + have := (tail_sublist l).le_countP p + simp only [length_tail] at this + omega + +variable [BEq α] + +theorem Sublist.le_count (s : l₁ <+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ := + s.le_countP _ + +theorem IsPrefix.le_count (s : l₁ <+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ := + s.sublist.le_count _ + +theorem IsSuffix.le_count (s : l₁ <:+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ := + s.sublist.le_count _ + +theorem IsInfix.le_count (s : l₁ <:+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ := + s.sublist.le_count _ + +theorem le_count_tail (a : α) (l) : count a l - 1 ≤ count a l.tail := + le_countP_tail _ + end List diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean index c8d1d62d52..3e87e55188 100644 --- a/src/Init/Data/List/Nat/Range.lean +++ b/src/Init/Data/List/Nat/Range.lean @@ -258,6 +258,9 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) := | zero => simp at h | succ n => simp +@[simp] theorem tail_iota (n : Nat) : (iota n).tail = iota (n - 1) := by + cases n <;> simp + @[simp] theorem reverse_iota : reverse (iota n) = range' 1 n := by induction n with | zero => simp @@ -448,6 +451,9 @@ theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) : l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a) := by simp [getLast?_eq_getElem?] +@[simp] theorem tail_enum (l : List α) : (enum l).tail = enumFrom 1 l.tail := by + simp [enum] + theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l[i]? = x := by simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub] diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean index 17c21844cf..02eb165c84 100644 --- a/src/Init/Data/List/Range.lean +++ b/src/Init/Data/List/Range.lean @@ -35,11 +35,16 @@ theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step) theorem range'_ne_nil (s : Nat) {n : Nat} : range' s n ≠ [] ↔ n ≠ 0 := by cases n <;> simp -@[simp] theorem range'_zero : range' s 0 = [] := by +@[simp] theorem range'_zero : range' s 0 step = [] := by simp @[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl +@[simp] theorem tail_range' (n : Nat) : (range' s n step).tail = range' (s + step) (n - 1) step := by + cases n with + | zero => simp + | succ n => simp [range'_succ] + @[simp] theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by constructor · intro h @@ -153,6 +158,9 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) := theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0 := by cases n <;> simp +@[simp] theorem tail_range (n : Nat) : (range n).tail = range' 1 (n - 1) := by + rw [range_eq_range', tail_range'] + @[simp] theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by simp only [range_eq_range', range'_sublist_right] @@ -219,6 +227,12 @@ theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).len simp only [getElem?_enumFrom, getElem?_eq_getElem h] simp +@[simp] +theorem tail_enumFrom (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail := by + induction l generalizing n with + | nil => simp + | cons _ l ih => simp [ih, enumFrom_cons] + theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) : map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l := ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean index 82de8c49e5..49019499a9 100644 --- a/src/Init/Data/List/Zip.lean +++ b/src/Init/Data/List/Zip.lean @@ -31,6 +31,10 @@ theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) : theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) : zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id] +@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) : + (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by + cases l₁ <;> cases l₂ <;> simp + theorem zip_append : ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂), zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂ @@ -229,6 +233,7 @@ theorem drop_zipWith : (zipWith f l l').drop n = zipWith f (l.drop n) (l'.drop n @[deprecated drop_zipWith (since := "2024-07-26")] abbrev zipWith_distrib_drop := @drop_zipWith +@[simp] theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail := by rw [← drop_one]; simp [drop_zipWith] @@ -284,12 +289,16 @@ theorem head?_zipWithAll {f : Option α → Option β → γ} : | none, none => .none | a?, b? => some (f a? b?) := by simp [head?_eq_getElem?, getElem?_zipWithAll] -theorem head_zipWithAll {f : Option α → Option β → γ} (h) : +@[simp] theorem head_zipWithAll {f : Option α → Option β → γ} (h) : (zipWithAll f as bs).head h = f as.head? bs.head? := by apply Option.some.inj rw [← head?_eq_head, head?_zipWithAll] split <;> simp_all +@[simp] theorem tail_zipWithAll {f : Option α → Option β → γ} : + (zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail := by + cases as <;> cases bs <;> simp + theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) : zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂ := by induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all @@ -358,6 +367,12 @@ theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp (hr : lp.map Prod.snd = l') : lp = l.zip l' := by rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip] +@[simp] theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1 := by + cases l <;> simp + +@[simp] theorem tail_zip_snd {l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2 := by + cases l <;> simp + @[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} : unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by ext1 <;> simp