Trigger CI for leanprover/lean4#4712

Batteries.lean

@@ -1,4 +1,3 @@
-import Batteries.Classes.BEq
 import Batteries.Classes.Cast
 import Batteries.Classes.Order
 import Batteries.Classes.RatCast
@@ -64,12 +63,10 @@ import Batteries.Lean.NameMapAttribute
 import Batteries.Lean.PersistentHashMap
 import Batteries.Lean.PersistentHashSet
 import Batteries.Lean.Position
-import Batteries.Lean.SMap
 import Batteries.Lean.Syntax
 import Batteries.Lean.System.IO
 import Batteries.Lean.TagAttribute
 import Batteries.Lean.Util.EnvSearch
-import Batteries.Lean.Util.Path
 import Batteries.Linter
 import Batteries.Linter.UnnecessarySeqFocus
 import Batteries.Linter.UnreachableTactic

Batteries/Data/Array/Merge.lean

@@ -27,7 +27,7 @@ where
   termination_by xs.size + ys.size - (i + j)
 
 set_option linter.unusedVariables false in
-@[deprecated merge, inherit_doc merge]
+@[deprecated merge (since := "2024-04-24"), inherit_doc merge]
 def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) : Array α :=
   merge (compare · · |>.isLT) xs ys
 
@@ -55,7 +55,7 @@ where
       | .eq => go (acc.push (merge x y)) (i + 1) (j + 1)
   termination_by xs.size + ys.size - (i + j)
 
-@[deprecated] alias mergeSortedMergingDuplicates := mergeDedupWith
+@[deprecated (since := "2024-04-24")] alias mergeSortedMergingDuplicates := mergeDedupWith
 
 /--
 `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
@@ -64,7 +64,7 @@ not contain duplicates. If an element appears in both `xs` and `ys`, only one co
 @[inline] def mergeDedup [ord : Ord α] (xs ys : Array α) : Array α :=
   mergeDedupWith (ord := ord) xs ys fun x _ => x
 
-@[deprecated] alias mergeSortedDeduplicating := mergeDedup
+@[deprecated (since := "2024-04-24")] alias mergeSortedDeduplicating := mergeDedup
 
 set_option linter.unusedVariables false in
 /--
@@ -83,7 +83,7 @@ where
     ys.foldl (init := xs) fun xs y =>
       if xs.any (· == y) (stop := xsSize) then xs else xs.push y
 
-@[deprecated] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
+@[deprecated (since := "2024-04-24")] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
 
 /--
 `O(|xs|)`. Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with
@@ -101,7 +101,7 @@ where
       acc.push hd
   termination_by xs.size - i
 
-@[deprecated] alias mergeAdjacentDuplicates := mergeAdjacentDups
+@[deprecated (since := "2024-04-24")] alias mergeAdjacentDuplicates := mergeAdjacentDups
 
 /--
 `O(|xs|)`. Deduplicate a sorted array. The array must be sorted with to an order which agrees with
@@ -110,13 +110,13 @@ where
 def dedupSorted [eq : BEq α] (xs : Array α) : Array α :=
   xs.mergeAdjacentDups (eq := eq) fun x _ => x
 
-@[deprecated] alias deduplicateSorted := dedupSorted
+@[deprecated (since := "2024-04-24")] alias deduplicateSorted := dedupSorted
 
 /-- `O(|xs| log |xs|)`. Sort and deduplicate an array. -/
 def sortDedup [ord : Ord α] (xs : Array α) : Array α :=
   have := ord.toBEq
   dedupSorted <| xs.qsort (compare · · |>.isLT)
 
-@[deprecated] alias sortAndDeduplicate := sortDedup
+@[deprecated (since := "2024-04-24")] alias sortAndDeduplicate := sortDedup
 
 end Array

Batteries/Data/BitVec/Lemmas.lean

@@ -7,13 +7,10 @@ import Batteries.Tactic.Alias
 
 namespace BitVec
 
-/-- Replaced 2024-02-07. -/
-@[deprecated] alias zero_is_unique := eq_nil
+@[deprecated (since := "2024-02-07")] alias zero_is_unique := eq_nil
 
 /-! ### sub/neg -/
 
-/-- Replaced 2024-02-06. -/
-@[deprecated] alias sub_toNat := toNat_sub
+@[deprecated (since := "2024-02-07")] alias sub_toNat := toNat_sub
 
-/-- Replaced 2024-02-06. -/
-@[deprecated] alias neg_toNat := toNat_neg
+@[deprecated (since := "2024-02-07")] alias neg_toNat := toNat_neg

Batteries/Data/Bool.lean

@@ -10,10 +10,10 @@ namespace Bool
 
 /-! ### injectivity lemmas -/
 
-@[deprecated] alias not_inj' := not_inj_iff
+@[deprecated (since := "2023-10-27")] alias not_inj' := not_inj_iff
 
-@[deprecated] alias and_or_inj_right' := and_or_inj_right_iff
+@[deprecated (since := "2023-10-27")] alias and_or_inj_right' := and_or_inj_right_iff
 
-@[deprecated] alias and_or_inj_left' := and_or_inj_left_iff
+@[deprecated (since := "2023-10-27")] alias and_or_inj_left' := and_or_inj_left_iff
 
 end Bool

Batteries/Data/HashMap/Basic.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura, Mario Carneiro
 import Batteries.Data.AssocList
 import Batteries.Data.Nat.Basic
 import Batteries.Data.Array.Monadic
-import Batteries.Classes.BEq
 
 namespace Batteries.HashMap
 

Batteries/Data/HashMap/Lemmas.lean

@@ -5,7 +5,13 @@ Authors: Scott Morrison
 -/
 import Batteries.Data.HashMap.Basic
 import Batteries.Data.Array.Lemmas
-import Batteries.Util.ProofWanted
+
+/-!
+# Lemmas for `Batteries.HashMap`
+
+Note that Lean core provides an alternative hash map implementation, `Std.HashMap`, which comes with
+more lemmas. See the module `Std.Data.HashMap.Lemmas`.
+-/
 
 namespace Batteries.HashMap
 
@@ -21,5 +27,7 @@ end Imp
 @[simp] theorem empty_find? [BEq α] [Hashable α] {a : α} :
     (∅ : HashMap α β).find? a = none := by simp [find?, Imp.find?]
 
-proof_wanted insert_find? [BEq α] [Hashable α] (m : HashMap α β) (a a' : α) (b : β) :
-    (m.insert a b).find? a' = if a' == a then some b else m.find? a'
+-- `Std.HashMap` has this lemma (as `getElem?_insert`) and many more, so working on this
+-- `proof_wanted` is likely not a good use of your time.
+-- proof_wanted insert_find? [BEq α] [Hashable α] (m : HashMap α β) (a a' : α) (b : β) :
+--     (m.insert a b).find? a' = if a' == a then some b else m.find? a'

Batteries/Data/HashMap/WF.lean

@@ -95,7 +95,7 @@ where
     · next H =>
       refine (go (i+1) _ _ fun j hj => ?a).trans ?b <;> simp
       · case a =>
-        simp [List.getD_eq_getElem?, List.getElem?_set, Option.map_eq_map]; split
+        simp [List.getD_eq_getElem?_getD, List.getElem?_set, Option.map_eq_map]; split
         · cases source.data[j]? <;> rfl
         · next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H))
       · case b =>

Batteries/Data/Int/Order.lean

@@ -7,4 +7,4 @@ import Batteries.Tactic.Alias
 
 namespace Int
 
-@[deprecated] alias ofNat_natAbs_eq_of_nonneg := natAbs_of_nonneg
+@[deprecated (since := "2024-01-24")] alias ofNat_natAbs_eq_of_nonneg := natAbs_of_nonneg

Batteries/Data/List/Basic.lean

@@ -10,16 +10,6 @@ namespace List
 
 /-! ## New definitions -/
 
-/--
-`l₁ ⊆ l₂` means that every element of `l₁` is also an element of `l₂`, ignoring multiplicity.
--/
-protected def Subset (l₁ l₂ : List α) := ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂
-
-instance : HasSubset (List α) := ⟨List.Subset⟩
-
-instance [DecidableEq α] : DecidableRel (Subset : List α → List α → Prop) :=
-  fun _ _ => decidableBAll _ _
-
 /--
 Computes the "bag intersection" of `l₁` and `l₂`, that is,
 the collection of elements of `l₁` which are also in `l₂`. As each element
@@ -93,9 +83,9 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
 /-- 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] alias removeNth := eraseIdx
-@[deprecated] alias removeNthTR := eraseIdxTR
-@[deprecated] alias removeNth_eq_removeNthTR := eraseIdx_eq_eraseIdxTR
+@[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
 
 /-- Replaces the first element of the list for which `f` returns `some` with the returned value. -/
 @[simp] def replaceF (f : α → Option α) : List α → List α
@@ -139,26 +129,6 @@ Unlike `bagInter` this does not preserve multiplicity: `[1, 1].inter [1]` is `[1
 
 instance [BEq α] : Inter (List α) := ⟨List.inter⟩
 
-/-- `l₁ <+ l₂`, or `Sublist l₁ l₂`, says that `l₁` is a (non-contiguous) subsequence of `l₂`. -/
-inductive Sublist {α} : List α → List α → Prop
-  /-- the base case: `[]` is a sublist of `[]` -/
-  | slnil : Sublist [] []
-  /-- If `l₁` is a subsequence of `l₂`, then it is also a subsequence of `a :: l₂`. -/
-  | cons a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
-  /-- If `l₁` is a subsequence of `l₂`, then `a :: l₁` is a subsequence of `a :: l₂`. -/
-  | cons₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
-
-@[inherit_doc] scoped infixl:50 " <+ " => Sublist
-
-/-- True if the first list is a potentially non-contiguous sub-sequence of the second list. -/
-def isSublist [BEq α] : List α → List α → Bool
-  | [], _ => true
-  | _, [] => false
-  | l₁@(hd₁::tl₁), hd₂::tl₂ =>
-    if hd₁ == hd₂
-    then tl₁.isSublist tl₂
-    else l₁.isSublist tl₂
-
 /--
 Split a list at an index.
 ```
@@ -299,7 +269,7 @@ theorem insertNthTR_go_eq : ∀ n l, insertNthTR.go a n l acc = acc.data ++ inse
 @[csimp] theorem insertNth_eq_insertNthTR : @insertNth = @insertNthTR := by
   funext α f n l; simp [insertNthTR, insertNthTR_go_eq]
 
-@[simp] theorem headD_eq_head? (l) (a : α) : headD l a = (head? l).getD a := by cases l <;> rfl
+theorem headD_eq_head? (l) (a : α) : headD l a = (head? l).getD a := by cases l <;> rfl
 
 /--
 Take `n` elements from a list `l`. If `l` has less than `n` elements, append `n - length l`
@@ -659,29 +629,6 @@ theorem sections_eq_nil_of_isEmpty : ∀ {L}, L.any isEmpty → @sections α L =
   rw [Array.foldl_eq_foldl_data, Array.foldl_data_eq_bind]; rfl
   intros; apply Array.foldl_data_eq_map
 
-/-- `eraseP p l` removes the first element of `l` satisfying the predicate `p`. -/
-def eraseP (p : α → Bool) : List α → List α
-  | [] => []
-  | a :: l => bif p a then l else a :: eraseP p l
-
-/-- Tail-recursive version of `eraseP`. -/
-@[inline] def erasePTR (p : α → Bool) (l : List α) : List α := go l #[] where
-  /-- Auxiliary for `erasePTR`: `erasePTR.go p l xs acc = acc.toList ++ eraseP p xs`,
-  unless `xs` does not contain any elements satisfying `p`, where it returns `l`. -/
-  @[specialize] go : List α → Array α → List α
-  | [], _ => l
-  | a :: l, acc => bif p a then acc.toListAppend l else go l (acc.push a)
-
-@[csimp] theorem eraseP_eq_erasePTR : @eraseP = @erasePTR := by
-  funext α p l; simp [erasePTR]
-  let rec go (acc) : ∀ xs, l = acc.data ++ xs →
-    erasePTR.go p l xs acc = acc.data ++ xs.eraseP p
-  | [] => fun h => by simp [erasePTR.go, eraseP, h]
-  | x::xs => by
-    simp [erasePTR.go, eraseP]; cases p x <;> simp
-    · intro h; rw [go _ xs]; {simp}; simp [h]
-  exact (go #[] _ rfl).symm
-
 /--
 `extractP p l` returns a pair of an element `a` of `l` satisfying the predicate
 `p`, and `l`, with `a` removed. If there is no such element `a` it returns `(none, l)`.
@@ -806,46 +753,6 @@ where
     rename_i a as b bs; unfold cond; cases R a b <;> simp [go as bs]
   exact (go as bs [] []).symm
 
-section Pairwise
-
-variable (R : α → α → Prop)
-
-/--
-`Pairwise R l` means that all the elements with earlier indexes are
-`R`-related to all the elements with later indexes.
-```
-Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
-```
-For example if `R = (·≠·)` then it asserts `l` has no duplicates,
-and if `R = (·<·)` then it asserts that `l` is (strictly) sorted.
--/
-inductive Pairwise : List α → Prop
-  /-- All elements of the empty list are vacuously pairwise related. -/
-  | nil : Pairwise []
-  /-- `a :: l` is `Pairwise R` if `a` `R`-relates to every element of `l`,
-  and `l` is `Pairwise R`. -/
-  | cons : ∀ {a : α} {l : List α}, (∀ a' ∈ l, R a a') → Pairwise l → Pairwise (a :: l)
-
-attribute [simp] Pairwise.nil
-
-variable {R}
-
-@[simp] theorem pairwise_cons : Pairwise R (a::l) ↔ (∀ a' ∈ l, R a a') ∧ Pairwise R l :=
-  ⟨fun | .cons h₁ h₂ => ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => h₂.cons h₁⟩
-
-instance instDecidablePairwise [DecidableRel R] :
-    (l : List α) → Decidable (Pairwise R l)
-  | [] => isTrue .nil
-  | hd :: tl =>
-    match instDecidablePairwise tl with
-    | isTrue ht =>
-      match decidableBAll (R hd) tl with
-      | isFalse hf => isFalse fun hf' => hf (pairwise_cons.1 hf').1
-      | isTrue ht' => isTrue <| pairwise_cons.mpr (And.intro ht' ht)
-    | isFalse hf => isFalse fun | .cons _ ih => hf ih
-
-end Pairwise
-
 /--
 `pwFilter R l` is a maximal sublist of `l` which is `Pairwise R`.
 `pwFilter (·≠·)` is the erase duplicates function (cf. `eraseDup`), and `pwFilter (·<·)` finds
@@ -881,13 +788,6 @@ def Chain' : List α → Prop
 
 end Chain
 
-/-- `Nodup l` means that `l` has no duplicates, that is, any element appears at most
-  once in the List. It is defined as `Pairwise (≠)`. -/
-def Nodup : List α → Prop := Pairwise (· ≠ ·)
-
-instance nodupDecidable [DecidableEq α] : ∀ l : List α, Decidable (Nodup l) :=
-  instDecidablePairwise
-
 /-- `eraseDup l` removes duplicates from `l` (taking only the first occurrence).
 Defined as `pwFilter (≠)`.
 
@@ -926,15 +826,15 @@ def range' : (start len : Nat) → (step : Nat := 1) → List Nat
 `ilast' x xs` returns the last element of `xs` if `xs` is non-empty; it returns `x` otherwise.
 Use `List.getLastD` instead.
 -/
-@[simp, deprecated getLastD] def ilast' {α} : α → List α → α
+@[simp, deprecated getLastD (since := "2024-01-09")] def ilast' {α} : α → List α → α
   | a, [] => a
   | _, b :: l => ilast' b l
 
 /--
 `last' xs` returns the last element of `xs` if `xs` is non-empty; it returns `none` otherwise.
 Use `List.getLast?` instead
 -/
-@[simp, deprecated getLast?] def last' {α} : List α → Option α
+@[simp, deprecated getLast? (since := "2024-01-09")] def last' {α} : List α → Option α
   | [] => none
   | [a] => some a
   | _ :: l => last' l

Batteries/Data/List/Count.lean

@@ -62,8 +62,8 @@ theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
   | nil => rfl
   | cons x l ih =>
     if h : p x
-    then rw [countP_cons_of_pos p l h, ih, filter_cons_of_pos l h, length]
-    else rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg l h]
+    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]
@@ -196,11 +196,11 @@ theorem filter_beq (l : List α) (a : α) : l.filter (· == a) = replicate (coun
 theorem filter_eq (l : List α) (a : α) : l.filter (· = a) = replicate (count a l) a :=
   filter_beq l a
 
-@[deprecated filter_eq]
+@[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]
+@[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