chore: bump toolchain to v4.17.0-rc1 (#1115)

Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Matthew Ballard <[email protected]>

Batteries/Classes/Order.lean

@@ -5,29 +5,6 @@ Authors: Mario Carneiro
 -/
 import Batteries.Tactic.SeqFocus
 
-/-! ## Ordering -/
-
-namespace Ordering
-
-@[simp] theorem swap_swap {o : Ordering} : o.swap.swap = o := by cases o <;> rfl
-
-@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ :=
-  ⟨fun h => by simpa using congrArg swap h, congrArg _⟩
-
-theorem swap_then (o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap := by
-  cases o₁ <;> rfl
-
-theorem then_eq_lt {o₁ o₂ : Ordering} : o₁.then o₂ = lt ↔ o₁ = lt ∨ o₁ = eq ∧ o₂ = lt := by
-  cases o₁ <;> cases o₂ <;> decide
-
-theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq ↔ o₁ = eq ∧ o₂ = eq := by
-  cases o₁ <;> simp [«then»]
-
-theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt ∨ o₁ = eq ∧ o₂ = gt := by
-  cases o₁ <;> cases o₂ <;> decide
-
-end Ordering
-
 namespace Batteries
 
 /-- `TotalBLE le` asserts that `le` has a total order, that is, `le a b ∨ le b a`. -/

Batteries/Data/Array/Lemmas.lean

@@ -26,13 +26,6 @@ theorem forIn_eq_forIn_toList [Monad m]
 @[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
-/-! ### filter -/
-
-theorem size_filter_le (p : α → Bool) (l : Array α) :
-    (l.filter p).size ≤ l.size := by
-  simp only [← length_toList, toList_filter]
-  apply List.length_filter_le
-
 /-! ### flatten -/
 
 @[deprecated (since := "2024-09-09")] alias data_join := toList_flatten
@@ -41,30 +34,22 @@ theorem size_filter_le (p : α → Bool) (l : Array α) :
 
 /-! ### indexOf? -/
 
-theorem indexOf?_toList [BEq α] {a : α} {l : Array α} :
-    l.toList.indexOf? a = (l.indexOf? a).map Fin.val := by
-  simpa using aux l 0
-where
-  aux (l : Array α) (i : Nat) :
-       ((l.toList.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
-    rw [indexOfAux]
-    if h : i < l.size then
-      rw [List.drop_eq_getElem_cons h, getElem_toList, List.indexOf?_cons]
-      if h' : l[i] == a then
-        simp [h, h']
-      else
-        simp [h, h', ←aux l (i+1), Function.comp_def, ←Nat.add_assoc, Nat.add_right_comm]
-    else
-      have h' : l.size ≤ i := Nat.le_of_not_lt h
-      simp [h, List.drop_of_length_le h', List.indexOf?]
-  termination_by l.size - i
+open List
+
+theorem idxOf?_toList [BEq α] {a : α} {l : Array α} :
+    l.toList.idxOf? a = l.idxOf? a := by
+  rcases l with ⟨l⟩
+  simp
 
 /-! ### erase -/
 
+@[deprecated (since := "2025-02-03")] alias eraseP_toArray := List.eraseP_toArray
+@[deprecated (since := "2025-02-03")] alias erase_toArray := List.erase_toArray
+
 @[simp] theorem toList_erase [BEq α] (l : Array α) (a : α) :
     (l.erase a).toList = l.toList.erase a := by
-  simp only [erase, ← List.eraseIdx_indexOf_eq_erase, List.indexOf_eq_indexOf?, length_toList]
-  cases h : l.indexOf? a <;> simp [Array.indexOf?_toList, List.eraseIdx_of_length_le, *]
+  rcases l with ⟨l⟩
+  simp
 
 @[simp] theorem size_eraseIdxIfInBounds (a : Array α) (i : Nat) :
     (a.eraseIdxIfInBounds i).size = if i < a.size then a.size-1 else a.size := by

Batteries/Data/Array/Monadic.lean

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Batteries.Classes.SatisfiesM
+import Batteries.Util.ProofWanted
 
 /-!
 # Results about monadic operations on `Array`, in terms of `SatisfiesM`.
@@ -59,6 +60,13 @@ theorem size_mapM [Monad m] [LawfulMonad m] (f : α → m β) (as : Array α) :
     SatisfiesM (fun arr => arr.size = as.size) (Array.mapM f as) :=
   (SatisfiesM_mapM' _ _ (fun _ _ => True) (fun _ => .trivial)).imp (·.1)
 
+proof_wanted size_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Nat → α → m β) :
+    SatisfiesM (fun arr => arr.size = as.size) (Array.mapIdxM f as)
+
+proof_wanted size_mapFinIdxM [Monad m] [LawfulMonad m]
+    (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → m β) :
+    SatisfiesM (fun arr => arr.size = as.size) (Array.mapFinIdxM as f)
+
 theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) (start stop)
     (hstart : start ≤ min stop as.size) (tru : Prop) (fal : Nat → Prop) (h0 : fal start)
     (hp : ∀ i : Fin as.size, i.1 < stop → fal i.1 →
@@ -125,39 +133,90 @@ theorem SatisfiesM_foldrM [Monad m] [LawfulMonad m]
   simp [foldrM]; split; {exact go _ h0}
   · next h => exact .pure (Nat.eq_zero_of_not_pos h ▸ h0)
 
-theorem SatisfiesM_mapFinIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Fin as.size → α → m β)
+theorem SatisfiesM_mapFinIdxM [Monad m] [LawfulMonad m] (as : Array α)
+    (f : (i : Nat) → α → (h : i < as.size) → m β)
     (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
-    (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f i as[i])) :
+    (p : (i : Nat) → β → (h : i < as.size) → Prop)
+    (hs : ∀ i h, motive i → SatisfiesM (p i · h ∧ motive (i + 1)) (f i as[i] h)) :
     SatisfiesM
-      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
+      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p i arr[i] h)
       (Array.mapFinIdxM as f) := by
-  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
+  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p i bs[i] h) (hm : motive j) :
     SatisfiesM
-      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
+      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p i arr[i] h)
       (Array.mapFinIdxM.map as f i j h bs) := by
     induction i generalizing j bs with simp [mapFinIdxM.map]
     | zero =>
       have := (Nat.zero_add _).symm.trans h
       exact .pure ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
     | succ i ih =>
-      refine (hs _ (by exact hm)).bind fun b hb => ih (by simp [h₁]) (fun i hi hi' => ?_) hb.2
+      refine (hs _ _ (by exact hm)).bind fun b hb => ih (by simp [h₁]) (fun i hi hi' => ?_) hb.2
       simp at hi'; simp [getElem_push]; split
       · next h => exact h₂ _ _ h
       · next h => cases h₁.symm ▸ (Nat.le_or_eq_of_le_succ hi').resolve_left h; exact hb.1
   simp [mapFinIdxM]; exact go rfl nofun h0
 
 theorem SatisfiesM_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Nat → α → m β)
     (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
-    (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f i as[i])) :
+    (p : (i : Nat) → β → (h : i < as.size) → Prop)
+    (hs : ∀ i h, motive i → SatisfiesM (p i · h ∧ motive (i + 1)) (f i as[i])) :
     SatisfiesM
-      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
+      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p i arr[i] h)
       (as.mapIdxM f) :=
-  SatisfiesM_mapFinIdxM as (fun i => f i) motive h0 p hs
+  SatisfiesM_mapFinIdxM as (fun i a _ => f i a) motive h0 p hs
 
 theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α → m α) :
     SatisfiesM (·.size = a.size) (a.modifyM i f) := by
   unfold modifyM; split
   · exact .bind_pre <| .of_true fun _ => .pure <| by simp only [size_set]
   · exact .pure rfl
+
+end Array
+
+namespace List
+
+proof_wanted filterM_toArray [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) :
+    l.toArray.filterM p = toArray <$> l.filterM p
+
+proof_wanted filterRevM_toArray [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) :
+    l.toArray.filterRevM p = toArray <$> l.filterRevM p
+
+proof_wanted filterMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Option β)) :
+    l.toArray.filterMapM f = toArray <$> l.filterMapM f
+
+proof_wanted flatMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Array β)) :
+    l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => toList <$> f a)
+
+proof_wanted mapFinIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
+    (f : (i : Nat) → α → (h : i < l.length) → m β) :
+    l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM (fun i a h => f i a (by simpa using h))
+
+proof_wanted mapIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
+    (f : Nat → α → m β) :
+    l.toArray.mapIdxM f = toArray <$> l.mapIdxM f
+
+end List
+
+namespace Array
+
+proof_wanted toList_filterM [Monad m] [LawfulMonad m] (a : Array α) (p : α → m Bool) :
+    toList <$> a.filterM p = a.toList.filterM p
+
+proof_wanted toList_filterRevM [Monad m] [LawfulMonad m] (a : Array α) (p : α → m Bool) :
+    toList <$> a.filterRevM p = a.toList.filterRevM p
+
+proof_wanted toList_filterMapM [Monad m] [LawfulMonad m] (a : Array α) (f : α → m (Option β)) :
+    toList <$> a.filterMapM f = a.toList.filterMapM f
+
+proof_wanted toList_flatMapM [Monad m] [LawfulMonad m] (a : Array α) (f : α → m (Array β)) :
+    toList <$> a.flatMapM f = a.toList.flatMapM (fun a => toList <$> f a)
+
+proof_wanted toList_mapFinIdxM [Monad m] [LawfulMonad m] (l : Array α)
+    (f : (i : Nat) → α → (h : i < l.size) → m β) :
+    toList <$> l.mapFinIdxM f = l.toList.mapFinIdxM (fun i a h => f i a (by simpa using h))
+
+proof_wanted toList_mapIdxM [Monad m] [LawfulMonad m] (l : Array α)
+    (f : Nat → α → m β) :
+    toList <$> l.mapIdxM f = l.toList.mapIdxM f
+
+end Array

Batteries/Data/ByteArray.lean

@@ -53,7 +53,7 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
   Array.size_set ..
 
 @[simp] theorem get_set_eq (a : ByteArray) (i : Fin a.size) (v : UInt8) : (a.set i v)[i.val] = v :=
-  Array.get_set_eq ..
+  Array.getElem_set_self _ _ _ _ (eq := rfl) _
 
 theorem get_set_ne (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size) (h : i.val ≠ j) :
     (a.set i v)[j]'(a.size_set .. ▸ hj) = a[j] :=
@@ -76,7 +76,7 @@ theorem set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) :
 
 @[simp] theorem data_append (a b : ByteArray) : (a ++ b).data = a.data ++ b.data := by
   rw [←append_eq]; simp [ByteArray.append, size]
-  rw [Array.extract_empty_of_stop_le_start (h:=Nat.le_add_right ..), Array.append_nil]
+  rw [Array.extract_empty_of_stop_le_start (h:=Nat.le_add_right ..), Array.append_empty]
 @[deprecated (since := "2024-08-13")] alias append_data := data_append
 
 theorem size_append (a b : ByteArray) : (a ++ b).size = a.size + b.size := by

Batteries/Data/List/Basic.lean

@@ -32,15 +32,6 @@ open Option Nat
   | [] => none
   | a :: l => some (a, l)
 
-/-- Monadic variant of `mapIdx`. -/
-@[inline] def mapIdxM {m : Type v → Type w} [Monad m]
-    (as : List α) (f : Nat → α → m β) : m (List β) := go as #[] where
-  /-- Auxiliary for `mapIdxM`:
-  `mapIdxM.go as f acc = acc.toList ++ [← f acc.size a₀, ← f (acc.size + 1) a₁, ...]` -/
-  @[specialize] go : List α → Array β → m (List β)
-  | [], acc => pure acc.toList
-  | a :: as, acc => do go as (acc.push (← f acc.size a))
-
 /--
 `after p xs` is the suffix of `xs` after the first element that satisfies
 `p`, not including that element.

Batteries/Data/List/Lemmas.lean

@@ -448,20 +448,23 @@ theorem indexesOf_cons [BEq α] : (x :: xs : List α).indexesOf y =
     bif x == y then 0 :: (xs.indexesOf y).map (· + 1) else (xs.indexesOf y).map (· + 1) := by
   simp [indexesOf, findIdxs_cons]
 
-@[simp] theorem eraseIdx_indexOf_eq_erase [BEq α] (a : α) (l : List α) :
-    l.eraseIdx (l.indexOf a) = l.erase a := by
+@[simp] theorem eraseIdx_idxOf_eq_erase [BEq α] (a : α) (l : List α) :
+    l.eraseIdx (l.idxOf a) = l.erase a := by
   induction l with
   | nil => rfl
   | cons x xs ih =>
-    rw [List.erase, indexOf_cons]
+    rw [List.erase, idxOf_cons]
     cases x == a <;> simp [ih]
 
-theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) :
-    xs.indexOf x ∈ xs.indexesOf x := by
+@[deprecated (since := "2025-01-30")]
+alias eraseIdx_indexOf_eq_erase := eraseIdx_idxOf_eq_erase
+
+theorem idxOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) :
+    xs.idxOf x ∈ xs.indexesOf x := by
   induction xs with
   | nil => simp_all
   | cons h t ih =>
-    simp [indexOf_cons, indexesOf_cons, cond_eq_if]
+    simp [idxOf_cons, indexesOf_cons, cond_eq_if]
     split <;> rename_i w
     · apply mem_cons_self
     · cases m
@@ -470,18 +473,15 @@ theorem indexOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈
         specialize ih m
         simpa
 
-@[simp] theorem indexOf?_nil [BEq α] : ([] : List α).indexOf? x = none := rfl
-theorem indexOf?_cons [BEq α] :
-    (x :: xs : List α).indexOf? y = if x == y then some 0 else (xs.indexOf? y).map Nat.succ := by
-  simp [indexOf?]
+@[deprecated (since := "2025-01-30")]
+alias indexOf_mem_indexesOf := idxOf_mem_indexesOf
 
-theorem indexOf?_eq_none_iff [BEq α] {a : α} {l : List α} :
-    l.indexOf? a = none ↔ ∀ x ∈ l, ¬x == a := by
-  simp [indexOf?, findIdx?_eq_none_iff]
+theorem idxOf_eq_idxOf? [BEq α] (a : α) (l : List α) :
+    l.idxOf a = (match l.idxOf? a with | some i => i | none => l.length) := by
+  simp [idxOf, idxOf?, findIdx_eq_findIdx?]
 
-theorem indexOf_eq_indexOf? [BEq α] (a : α) (l : List α) :
-    l.indexOf a = (match l.indexOf? a with | some i => i | none => l.length) := by
-  simp [indexOf, indexOf?, findIdx_eq_findIdx?]
+@[deprecated (since := "2025-01-30")]
+alias indexOf_eq_indexOf? := idxOf_eq_idxOf?
 
 /-! ### insertP -/
 
@@ -563,7 +563,7 @@ theorem dropInfix?_go_eq_some_iff [BEq α] {i l acc p s : List α} :
   unfold dropInfix?.go
   split
   · simp only [isEmpty_eq_true, ite_none_right_eq_some, some.injEq, Prod.mk.injEq, nil_eq,
-      append_assoc, append_eq_nil, ge_iff_le, and_imp]
+      append_assoc, append_eq_nil_iff, ge_iff_le, and_imp]
     constructor
     · rintro ⟨rfl, rfl, rfl⟩
       simp

Batteries/Data/List/Perm.lean

@@ -275,20 +275,6 @@ theorem Subperm.cons_left {l₁ l₂ : List α} (h : l₁ <+~ l₂) (x : α) (hx
     refine h y ?_
     simpa [hy'] using hy
 
-theorem perm_insertIdx {α} (x : α) (l : List α) {n} (h : n ≤ l.length) :
-    insertIdx n x l ~ x :: l := by
-  induction l generalizing n with
-  | nil =>
-    cases n with
-    | zero => rfl
-    | succ => cases h
-  | cons _ _ ih =>
-    cases n with
-    | zero => simp [insertIdx]
-    | succ =>
-      simp only [insertIdx, modifyTailIdx]
-      refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)
-
 @[deprecated (since := "2024-10-21")] alias perm_insertNth := perm_insertIdx
 
 theorem Perm.union_right {l₁ l₂ : List α} (t₁ : List α) (h : l₁ ~ l₂) : l₁ ∪ t₁ ~ l₂ ∪ t₁ := by
@@ -334,22 +320,4 @@ theorem perm_insertP (p : α → Bool) (a l) : insertP p a l ~ a :: l := by
 theorem Perm.insertP (p : α → Bool) (a) (h : l₁ ~ l₂) : insertP p a l₁ ~ insertP p a l₂ :=
   Perm.trans (perm_insertP ..) <| Perm.trans (Perm.cons _ h) <| Perm.symm (perm_insertP ..)
 
-theorem perm_merge (s : α → α → Bool) (l r) : merge l r s ~ l ++ r := by
-  match l, r with
-  | [], r => simp
-  | l, [] => simp
-  | a::l, b::r =>
-    rw [cons_merge_cons]
-    split
-    · apply Perm.trans ((perm_cons a).mpr (perm_merge s l (b::r)))
-      simp [cons_append]
-    · apply Perm.trans ((perm_cons b).mpr (perm_merge s (a::l) r))
-      simp [cons_append]
-      apply Perm.trans (Perm.swap ..)
-      apply Perm.cons
-      apply perm_cons_append_cons
-      exact Perm.rfl
-
-theorem Perm.merge (s₁ s₂ : α → α → Bool) (hl : l₁ ~ l₂) (hr : r₁ ~ r₂) :
-    merge l₁ r₁ s₁ ~ merge l₂ r₂ s₂ :=
-  Perm.trans (perm_merge ..) <| Perm.trans (Perm.append hl hr) <| Perm.symm (perm_merge ..)
+@[deprecated (since := "2025-01-04")] alias perm_merge := merge_perm_append

Batteries/Data/RBMap/Lemmas.lean

@@ -288,7 +288,7 @@ theorem size_eq {t : RBNode α} : t.size = t.toList.length := by
 @[simp] theorem Any_reverse {t : RBNode α} : t.reverse.Any p ↔ t.Any p := by simp [Any_def]
 
 @[simp] theorem memP_reverse {t : RBNode α} : MemP cut t.reverse ↔ MemP (cut · |>.swap) t := by
-  simp [MemP]; apply Iff.of_eq; congr; funext x; rw [← Ordering.swap_inj]; rfl
+  simp [MemP]
 
 theorem Mem_reverse [@OrientedCmp α cmp] {t : RBNode α} :
     Mem cmp x t.reverse ↔ Mem (flip cmp) x t := by

Batteries/Data/String/Lemmas.lean

@@ -429,9 +429,11 @@ theorem splitAux_of_valid (p l m r acc) :
             extract_of_valid l m (c :: r)⟩ :
           _ ∧ _ ∧ _),
       List.splitOnP.go, List.reverse_reverse]
-    split
-    · simpa [Nat.add_assoc] using splitAux_of_valid p (l++m++[c]) [] r (⟨m⟩::acc)
-    · simpa [Nat.add_assoc] using splitAux_of_valid p l (m++[c]) r acc
+    split <;> rename_i h
+    · simp_all only [List.head?_cons, Option.getD_some]
+      simpa [Nat.add_assoc] using splitAux_of_valid p (l++m++[c]) [] r (⟨m⟩::acc)
+    · simp_all only [List.head?_cons, Option.getD_some]
+      simpa [Nat.add_assoc] using splitAux_of_valid p l (m++[c]) r acc
 
 theorem split_of_valid (s p) : split s p = (List.splitOnP p s.1).map mk := by
   simpa [split] using splitAux_of_valid p [] [] s.1 []

Batteries/Data/Vector.lean

@@ -1,2 +1,3 @@
 import Batteries.Data.Vector.Basic
 import Batteries.Data.Vector.Lemmas
+import Batteries.Data.Vector.Monadic

Batteries/Data/Vector/Basic.lean

@@ -31,8 +31,6 @@ namespace Vector
 
 @[deprecated (since := "2024-11-24")] alias swapAtN := swapAt
 
-@[deprecated (since := "2024-10-22")] alias shrink := take
-
 @[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
 /-- Use `#v[]` instead. -/