feat: lemmas about List.tail (#5360)

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

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 _
 

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
 

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} :

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

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]
 

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

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