remove upstreamed material

Batteries/Data/List/Basic.lean

@@ -27,15 +27,6 @@ protected def diff {α} [BEq α] : List α → List α → List α
 
 open Option Nat
 
-/-- Get the tail of a nonempty list, or return `[]` for `[]`. -/
-def tail : List α → List α
-  | []    => []
-  | _::as => as
-
--- FIXME: `@[simp]` on the definition simplifies even `tail l`
-@[simp] theorem tail_nil : @tail α [] = [] := rfl
-@[simp] theorem tail_cons : @tail α (a::as) = as := rfl
-
 /-- Get the head and tail of a list, if it is nonempty. -/
 @[inline] def next? : List α → Option (α × List α)
   | [] => none
@@ -73,16 +64,6 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
   | [] => []
   | x :: xs => bif p x then xs else after p xs
 
-/-- Returns the index of the first element satisfying `p`, or the length of the list otherwise. -/
-@[inline] def findIdx (p : α → Bool) (l : List α) : Nat := go l 0 where
-  /-- Auxiliary for `findIdx`: `findIdx.go p l n = findIdx p l + n` -/
-  @[specialize] go : List α → Nat → Nat
-  | [], n => n
-  | a :: l, n => bif p a then n else go l (n + 1)
-
-/-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
-def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
-
 @[deprecated (since := "2024-05-06")] alias removeNth := eraseIdx
 @[deprecated (since := "2024-05-06")] alias removeNthTR := eraseIdxTR
 @[deprecated (since := "2024-05-06")] alias removeNth_eq_removeNthTR := eraseIdx_eq_eraseIdxTR
@@ -302,19 +283,6 @@ theorem takeDTR_go_eq : ∀ n l, takeDTR.go dflt n l acc = acc.data ++ takeD n l
 @[csimp] theorem takeD_eq_takeDTR : @takeD = @takeDTR := by
   funext α f n l; simp [takeDTR, takeDTR_go_eq]
 
-/--
-Pads `l : List α` with repeated occurrences of `a : α` until it is of length `n`.
-If `l` is initially larger than `n`, just return `l`.
--/
-def leftpad (n : Nat) (a : α) (l : List α) : List α := replicate (n - length l) a ++ l
-
-/-- Optimized version of `leftpad`. -/
-@[inline] def leftpadTR (n : Nat) (a : α) (l : List α) : List α :=
-  replicateTR.loop a (n - length l) l
-
-@[csimp] theorem leftpad_eq_leftpadTR : @leftpad = @leftpadTR := by
-  funext α n a l; simp [leftpad, leftpadTR, replicateTR_loop_eq]
-
 /--
 Fold a function `f` over the list from the left, returning the list of partial results.
 ```
@@ -386,14 +354,6 @@ indexesOf a [a, b, a, a] = [0, 2, 3]
 -/
 @[inline] def indexesOf [BEq α] (a : α) : List α → List Nat := findIdxs (· == a)
 
-/-- Return the index of the first occurrence of an element satisfying `p`. -/
-def findIdx? (p : α → Bool) : List α → (start : Nat := 0) → Option Nat
-| [], _ => none
-| a :: l, i => if p a then some i else findIdx? p l (i + 1)
-
-/-- Return the index of the first occurrence of `a` in the list. -/
-@[inline] def indexOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a)
-
 /--
 `lookmap` is a combination of `lookup` and `filterMap`.
 `lookmap f l` will apply `f : α → Option α` to each element of the list,
@@ -407,16 +367,6 @@ replacing `a → b` at the first value `a` in the list such that `f a = some b`.
     | some b => acc.toListAppend (b :: l)
     | none => go l (acc.push a)
 
-/-- `countP p l` is the number of elements of `l` that satisfy `p`. -/
-@[inline] def countP (p : α → Bool) (l : List α) : Nat := go l 0 where
-  /-- Auxiliary for `countP`: `countP.go p l acc = countP p l + acc`. -/
-  @[specialize] go : List α → Nat → Nat
-  | [], acc => acc
-  | x :: xs, acc => bif p x then go xs (acc + 1) else go xs acc
-
-/-- `count a l` is the number of occurrences of `a` in `l`. -/
-@[inline] def count [BEq α] (a : α) : List α → Nat := countP (· == a)
-
 /--
 `inits l` is the list of initial segments of `l`.
 ```
@@ -770,34 +720,6 @@ Defined as `pwFilter (≠)`.
     eraseDup [1, 0, 2, 2, 1] = [0, 2, 1] -/
 @[inline] def eraseDup [BEq α] : List α → List α := pwFilter (· != ·)
 
-/-- `range' start len step` is the list of numbers `[start, start+step, ..., start+(len-1)*step]`.
-  It is intended mainly for proving properties of `range` and `iota`. -/
-def range' : (start len : Nat) → (step : Nat := 1) → List Nat
-  | _, 0, _ => []
-  | s, n+1, step => s :: range' (s+step) n step
-
-/-- Optimized version of `range'`. -/
-@[inline] def range'TR (s n : Nat) (step : Nat := 1) : List Nat := go n (s + step * n) [] where
-  /-- Auxiliary for `range'TR`: `range'TR.go n e = [e-n, ..., e-1] ++ acc`. -/
-  go : Nat → Nat → List Nat → List Nat
-  | 0, _, acc => acc
-  | n+1, e, acc => go n (e-step) ((e-step) :: acc)
-
-@[csimp] theorem range'_eq_range'TR : @range' = @range'TR := by
-  funext s n step
-  let rec go (s) : ∀ n m,
-    range'TR.go step n (s + step * n) (range' (s + step * n) m step) = range' s (n + m) step
-  | 0, m => by simp [range'TR.go]
-  | n+1, m => by
-    simp [range'TR.go]
-    rw [Nat.mul_succ, ← Nat.add_assoc, Nat.add_sub_cancel, Nat.add_right_comm n]
-    exact go s n (m + 1)
-  exact (go s n 0).symm
-
-/-- Drop `none`s from a list, and replace each remaining `some a` with `a`. -/
-@[inline] def reduceOption {α} : List (Option α) → List α :=
-  List.filterMap id
-
 /--
 `ilast' x xs` returns the last element of `xs` if `xs` is non-empty; it returns `x` otherwise.
 Use `List.getLastD` instead.

Batteries/Data/List/Count.lean

@@ -19,230 +19,21 @@ open Nat
 
 namespace List
 
-section countP
-
-variable (p q : α → Bool)
-
-@[simp] theorem countP_nil : countP p [] = 0 := rfl
-
-protected theorem countP_go_eq_add (l) : countP.go p l n = n + countP.go p l 0 := by
-  induction l generalizing n with
-  | nil => rfl
-  | cons head tail ih =>
-    unfold countP.go
-    rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
-    if h : p head then simp [h, Nat.add_assoc] else simp [h]
-
-@[simp] theorem countP_cons_of_pos (l) (pa : p a) : countP p (a :: l) = countP p l + 1 := by
-  have : countP.go p (a :: l) 0 = countP.go p l 1 := show cond .. = _ by rw [pa]; rfl
-  unfold countP
-  rw [this, Nat.add_comm, List.countP_go_eq_add]
-
-@[simp] theorem countP_cons_of_neg (l) (pa : ¬p a) : countP p (a :: l) = countP p l := by
-  simp [countP, countP.go, pa]
-
-theorem countP_cons (a : α) (l) : countP p (a :: l) = countP p l + if p a then 1 else 0 := by
-  by_cases h : p a <;> simp [h]
-
-theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a => ¬p a) l := by
-  induction l with
-  | nil => rfl
-  | cons x h ih =>
-    if h : p x then
-      rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
-      · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
-      · simp only [h, not_true_eq_false, decide_False, not_false_eq_true]
-    else
-      rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
-      · rfl
-      · simp only [h, not_false_eq_true, decide_True]
-
-theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
-  induction l with
-  | nil => rfl
-  | cons x l ih =>
-    if h : p x
-    then rw [countP_cons_of_pos p l h, ih, filter_cons_of_pos h, length]
-    else rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg h]
-
-theorem countP_le_length : countP p l ≤ l.length := by
-  simp only [countP_eq_length_filter]
-  apply length_filter_le
-
-@[simp] theorem countP_append (l₁ l₂) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
-  simp only [countP_eq_length_filter, filter_append, length_append]
-
-theorem countP_pos : 0 < countP p l ↔ ∃ a ∈ l, p a := by
-  simp only [countP_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]
-
-theorem countP_eq_zero : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
-  simp only [countP_eq_length_filter, length_eq_zero, filter_eq_nil]
-
-theorem countP_eq_length : countP p l = l.length ↔ ∀ a ∈ l, p a := by
-  rw [countP_eq_length_filter, filter_length_eq_length]
-
-theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ := by
-  simp only [countP_eq_length_filter]
-  apply s.filter _ |>.length_le
-
-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]
-
-@[simp] theorem countP_true {l : List α} : (l.countP fun _ => true) = l.length := by
-  rw [countP_eq_length]
-  simp
-
-@[simp] theorem countP_false {l : List α} : (l.countP fun _ => false) = 0 := by
-  rw [countP_eq_zero]
-  simp
-
-@[simp] theorem countP_map (p : β → Bool) (f : α → β) :
-    ∀ l, countP p (map f l) = countP (p ∘ f) l
-  | [] => rfl
-  | a :: l => by rw [map_cons, countP_cons, countP_cons, countP_map p f l]; rfl
-
-variable {p q}
-
-theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by
-  induction l with
-  | nil => apply Nat.le_refl
-  | cons a l ihl =>
-    rw [forall_mem_cons] at h
-    have ⟨ha, hl⟩ := h
-    simp [countP_cons]
-    cases h : p a
-    . simp
-      apply Nat.le_trans ?_ (Nat.le_add_right _ _)
-      apply ihl hl
-    . simp [ha h]
-      apply ihl hl
-
-theorem countP_congr (h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l :=
-  Nat.le_antisymm
-    (countP_mono_left fun x hx => (h x hx).1)
-    (countP_mono_left fun x hx => (h x hx).2)
-
-end countP
 
 /-! ### count -/
 
 section count
 
 variable [DecidableEq α]
 
-@[simp] theorem count_nil (a : α) : count a [] = 0 := rfl
-
-theorem count_cons (a b : α) (l : List α) :
-    count a (b :: l) = count a l + if a = b then 1 else 0 := by
-  simp [count, countP_cons, eq_comm (a := a)]
-
-@[simp] theorem count_cons_self (a : α) (l : List α) : count a (a :: l) = count a l + 1 := by
-  simp [count_cons]
-
-@[simp] theorem count_cons_of_ne (h : a ≠ b) (l : List α) : count a (b :: l) = count a l := by
-  simp [count_cons, h]
-
-theorem count_tail : ∀ (l : List α) (a : α) (h : l ≠ []),
-      l.tail.count a = l.count a - if a = l.head h then 1 else 0
-  | head :: tail, a, h => by simp [count_cons]
-
-theorem count_le_length (a : α) (l : List α) : count a l ≤ l.length := countP_le_length _
-
-theorem Sublist.count_le (h : l₁ <+ l₂) (a : α) : count a l₁ ≤ count a l₂ := h.countP_le _
-
-theorem count_le_count_cons (a b : α) (l : List α) : count a l ≤ count a (b :: l) :=
-  (sublist_cons_self _ _).count_le _
-
-theorem count_singleton (a : α) : count a [a] = 1 := by simp
-
-theorem count_singleton' (a b : α) : count a [b] = if a = b then 1 else 0 := by simp [count_cons]
-
-@[simp] theorem count_append (a : α) : ∀ l₁ l₂, count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
-  countP_append _
+theorem count_singleton' (a b : α) : count a [b] = if b = a then 1 else 0 := by simp [count_cons]
 
 theorem count_concat (a : α) (l : List α) : count a (concat l a) = succ (count a l) := by simp
 
-@[simp]
-theorem count_pos_iff_mem {a : α} {l : List α} : 0 < count a l ↔ a ∈ l := by
-  simp only [count, countP_pos, beq_iff_eq, exists_eq_right]
-
-@[simp 900] theorem count_eq_zero_of_not_mem {a : α} {l : List α} (h : a ∉ l) : count a l = 0 :=
-  Decidable.byContradiction fun h' => h <| count_pos_iff_mem.1 (Nat.pos_of_ne_zero h')
-
-theorem not_mem_of_count_eq_zero {a : α} {l : List α} (h : count a l = 0) : a ∉ l :=
-  fun h' => Nat.ne_of_lt (count_pos_iff_mem.2 h') h.symm
-
-theorem count_eq_zero {l : List α} : count a l = 0 ↔ a ∉ l :=
-  ⟨not_mem_of_count_eq_zero, count_eq_zero_of_not_mem⟩
-
-theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b := by
-  rw [count, countP_eq_length]
-  refine ⟨fun h b hb => Eq.symm ?_, fun h b hb => ?_⟩
-  · simpa using h b hb
-  · rw [h b hb, beq_self_eq_true]
-
-@[simp] theorem count_replicate_self (a : α) (n : Nat) : count a (replicate n a) = n :=
-  (count_eq_length.2 <| fun _ h => (eq_of_mem_replicate h).symm).trans (length_replicate ..)
-
-theorem count_replicate (a b : α) (n : Nat) : count a (replicate n b) = if a = b then n else 0 := by
-  split
-  exacts [‹a = b› ▸ count_replicate_self .., count_eq_zero.2 <| mt eq_of_mem_replicate ‹a ≠ b›]
-
-theorem filter_beq (l : List α) (a : α) : l.filter (· == a) = replicate (count a l) a := by
-  simp only [count, countP_eq_length_filter, eq_replicate, mem_filter, beq_iff_eq]
-  exact ⟨trivial, fun _ h => h.2⟩
-
-theorem filter_eq (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a :=
-  filter_beq l a
-
 @[deprecated filter_eq (since := "2023-12-14")]
 theorem filter_eq' (l : List α) (a : α) : l.filter (a = ·) = replicate (count a l) a := by
   simpa only [eq_comm] using filter_eq l a
 
 @[deprecated filter_beq (since := "2023-12-14")]
 theorem filter_beq' (l : List α) (a : α) : l.filter (a == ·) = replicate (count a l) a := by
   simpa only [eq_comm (b := a)] using filter_eq l a
-
-theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l := by
-  refine ⟨fun h => ?_, fun h => ?_⟩
-  · exact ((replicate_sublist_replicate a).2 h).trans <| filter_eq l a ▸ filter_sublist _
-  · simpa only [count_replicate_self] using h.count_le a
-
-theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = length l) :
-    replicate (count a l) a = l :=
-  (le_count_iff_replicate_sublist.mp (Nat.le_refl _)).eq_of_length <|
-    (length_replicate (count a l) a).trans h
-
-@[simp] theorem count_filter {l : List α} (h : p a) : count a (filter p l) = count a l := by
-  rw [count, countP_filter]; congr; funext b
-  rw [(by rfl : (b == a) = decide (b = a)), decide_eq_decide]
-  simp; rintro rfl; exact h
-
-theorem count_le_count_map [DecidableEq β] (l : List α) (f : α → β) (x : α) :
-    count x l ≤ count (f x) (map f l) := by
-  rw [count, count, countP_map]
-  apply countP_mono_left; simp (config := { contextual := true })
-
-theorem count_erase (a b : α) :
-    ∀ l : List α, count a (l.erase b) = count a l - if a = b then 1 else 0
-  | [] => by simp
-  | c :: l => by
-    rw [erase_cons]
-    if hc : c = b then
-      have hc_beq := (beq_iff_eq _ _).mpr hc
-      rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
-    else
-      have hc_beq := beq_false_of_ne hc
-      simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
-      if ha : a = b then
-        rw [← ha, eq_comm] at hc
-        rw [if_pos ha, if_neg hc, Nat.add_zero, Nat.add_zero]
-      else
-        rw [if_neg ha, Nat.sub_zero, Nat.sub_zero]
-
-@[simp] theorem count_erase_self (a : α) (l : List α) :
-    count a (List.erase l a) = count a l - 1 := by rw [count_erase, if_pos rfl]
-
-@[simp] theorem count_erase_of_ne (ab : a ≠ b) (l : List α) : count a (l.erase b) = count a l := by
-  rw [count_erase, if_neg ab, Nat.sub_zero]