chore: bump toolchain to v4.18.0-rc1 (#1151)

Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Matthew Ballard <[email protected]> Co-authored-by: Markus Himmel <[email protected]> Co-authored-by: Kyle Miller <[email protected]> Co-authored-by: Mario Carneiro <[email protected]>
leanprover-community · Mar 3, 2025 · 092b30d · 092b30d
1 parent efcc7d9
commit 092b30d
Show file tree

Hide file tree

Showing 26 changed files with 125 additions and 414 deletions.
diff --git a/Batteries/Classes/Order.lean b/Batteries/Classes/Order.lean
@@ -37,7 +37,7 @@ theorem cmp_refl [OrientedCmp cmp] : cmp x x = .eq :=
 end OrientedCmp
 
 /-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/
-class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class TransCmp (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- The comparator operation is transitive. -/
   le_trans : cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt
 
@@ -99,15 +99,15 @@ theorem BEqCmp.cmp_iff_eq [BEq α] [LawfulBEq α] [BEqCmp (α := α) cmp] : cmp
   simp [BEqCmp.cmp_iff_beq]
 
 /-- `LTCmp cmp` asserts that `cmp x y = .lt` and `x < y` coincide. -/
-class LTCmp [LT α] (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class LTCmp [LT α] (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- `cmp x y = .lt` holds iff `x < y` is true. -/
   cmp_iff_lt : cmp x y = .lt ↔ x < y
 
 theorem LTCmp.cmp_iff_gt [LT α] [LTCmp (α := α) cmp] : cmp x y = .gt ↔ y < x := by
   rw [OrientedCmp.cmp_eq_gt, LTCmp.cmp_iff_lt]
 
 /-- `LECmp cmp` asserts that `cmp x y ≠ .gt` and `x ≤ y` coincide. -/
-class LECmp [LE α] (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class LECmp [LE α] (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- `cmp x y ≠ .gt` holds iff `x ≤ y` is true. -/
   cmp_iff_le : cmp x y ≠ .gt ↔ x ≤ y
 
@@ -116,8 +116,8 @@ theorem LECmp.cmp_iff_ge [LE α] [LECmp (α := α) cmp] : cmp x y ≠ .lt ↔ y
 
 /-- `LawfulCmp cmp` asserts that the `LE`, `LT`, `BEq` instances are all coherent with each other
 and with `cmp`, describing a strict weak order (a linear order except for antisymmetry). -/
-class LawfulCmp [LE α] [LT α] [BEq α] (cmp : α → α → Ordering) extends
-  TransCmp cmp, BEqCmp cmp, LTCmp cmp, LECmp cmp : Prop
+class LawfulCmp [LE α] [LT α] [BEq α] (cmp : α → α → Ordering) : Prop extends
+  TransCmp cmp, BEqCmp cmp, LTCmp cmp, LECmp cmp
 
 /-- `OrientedOrd α` asserts that the `Ord` instance satisfies `OrientedCmp`. -/
 abbrev OrientedOrd (α) [Ord α] := OrientedCmp (α := α) compare

diff --git a/Batteries/CodeAction/Misc.lean b/Batteries/CodeAction/Misc.lean
@@ -290,7 +290,7 @@ def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
   let (targets, induction, using_, alts) ← match info.stx with
     | `(tactic| cases $[$[$_ :]? $targets],* $[using $u]? $(alts)?) =>
       pure (targets, false, u, alts)
-    | `(tactic| induction $[$targets],* $[using $u]? $[generalizing $_*]? $(alts)?) =>
+    | `(tactic| induction $[$[$_ :]? $targets],* $[using $u]? $[generalizing $_*]? $(alts)?) =>
       pure (targets, true, u, alts)
     | _ => return #[]
   let some discrInfos := targets.mapM (findTermInfo? node) | return #[]

diff --git a/Batteries/Control/Monad.lean b/Batteries/Control/Monad.lean
@@ -3,35 +3,9 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Batteries.Tactic.Alias
 
--- Note: this will be replaced by `_root_.map_inj_right_of_nonempty` in nightly-2025-02-07
-theorem _root_.LawfulFunctor.map_inj_right_of_nonempty [Functor f] [LawfulFunctor f] [Nonempty α]
-    {g : α → β} (h : ∀ {x y : α}, g x = g y → x = y) {x y : f α} :
-    g <$> x = g <$> y ↔ x = y := by
-  constructor
-  · open Classical in
-    let g' a := if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
-    have g'g a : g' (g a) = a := by
-      simp only [exists_apply_eq_apply, ↓reduceDIte, g']
-      exact h (_ : ∃ b, g b = g a).choose_spec
-    intro h'
-    simpa only [Functor.map_map, g'g, id_map'] using congrArg (g' <$> ·) h'
-  · intro h'
-    rw [h']
-
--- Note: this will be replaced by `_root_.map_inj_right` in nightly-2025-02-07
-theorem _root_.LawfulMonad.map_inj_right [Monad m] [LawfulMonad m]
-    {f : α → β} (h : ∀ {x y : α}, f x = f y → x = y) {x y : m α} :
-    f <$> x = f <$> y ↔ x = y := by
-  by_cases hempty : Nonempty α
-  · exact LawfulFunctor.map_inj_right_of_nonempty h
-  · constructor
-    · intro h'
-      have (z : m α) : z = (do let a ← z; let b ← pure (f a); x) := by
-        conv => lhs; rw [← bind_pure z]
-        congr; funext a
-        exact (hempty ⟨a⟩).elim
-      rw [this x, this y]
-      rw [← bind_assoc, ← map_eq_pure_bind, h', map_eq_pure_bind, bind_assoc]
-    · intro h'
-      rw [h']
+@[deprecated (since := "2025-02-09")] alias LawfulFunctor.map_inj_right_of_nonempty :=
+map_inj_right_of_nonempty
+@[deprecated (since := "2025-02-09")] alias LawfulMonad.map_inj_right :=
+map_inj_right
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
@@ -43,8 +43,8 @@ theorem idxOf?_toList [BEq α] {a : α} {l : Array α} :
 
 /-! ### erase -/
 
-@[deprecated (since := "2025-02-03")] alias eraseP_toArray := List.eraseP_toArray
-@[deprecated (since := "2025-02-03")] alias erase_toArray := List.erase_toArray
+@[deprecated (since := "2025-02-06")] alias eraseP_toArray := List.eraseP_toArray
+@[deprecated (since := "2025-02-06")] alias erase_toArray := List.erase_toArray
 
 @[simp] theorem toList_erase [BEq α] (l : Array α) (a : α) :
     (l.erase a).toList = l.toList.erase a := by
@@ -65,137 +65,11 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
 
 /-! ### insertAt -/
 
-@[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) :
-    (insertIdx.loop i as j).size = as.size := by
-  unfold insertIdx.loop
-  split
-  · rw [size_insertIdx_loop, size_swap]
-  · rfl
-
-@[simp] theorem size_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
-    (as.insertIdx i v).size = as.size + 1 := by
-  rw [insertIdx, size_insertIdx_loop, size_push]
-
-@[deprecated size_insertIdx (since := "2024-11-20")] alias size_insertAt := size_insertIdx
-
-theorem getElem_insertIdx_loop_lt {as : Array α} {i : Nat} {j : Fin as.size} {k : Nat} {h}
-    (w : k < i) :
-    (insertIdx.loop i as j)[k] = as[k]'(by simpa using h) := by
-  unfold insertIdx.loop
-  split <;> rename_i h₁
-  · simp only
-    rw [getElem_insertIdx_loop_lt w]
-    rw [getElem_swap]
-    split <;> rename_i h₂
-    · simp_all
-      omega
-    · split <;> rename_i h₃
-      · omega
-      · simp_all
-  · rfl
-
-theorem getElem_insertIdx_loop_eq {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {h} :
-    (insertIdx.loop i as ⟨j, hj⟩)[i] = if i ≤ j then as[j] else as[i]'(by simpa using h) := by
-  unfold insertIdx.loop
-  split <;> rename_i h₁
-  · simp at h₁
-    have : j - 1 < j := by omega
-    rw [getElem_insertIdx_loop_eq]
-    rw [getElem_swap]
-    simp
-    split <;> rename_i h₂
-    · rw [if_pos (by omega)]
-    · omega
-  · simp at h₁
-    by_cases h' : i = j
-    · simp [h']
-    · have t : ¬ i ≤ j := by omega
-      simp [t]
-
-theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size}
-    {k : Nat} {h} (w : i < k) :
-    (insertIdx.loop i as ⟨j, hj⟩)[k] =
-      if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
-  unfold insertIdx.loop
-  split <;> rename_i h₁
-  · simp only
-    simp only at h₁
-    have : j - 1 < j := by omega
-    rw [getElem_insertIdx_loop_gt w]
-    rw [getElem_swap]
-    split <;> rename_i h₂
-    · rw [if_neg (by omega), if_neg (by omega)]
-      have t : k ≤ j := by omega
-      simp [t]
-    · rw [getElem_swap]
-      rw [if_neg (by omega)]
-      split <;> rename_i h₃
-      · simp [h₃]
-      · have t : ¬ k ≤ j := by omega
-        simp [t]
-  · simp only at h₁
-    have t : ¬ k ≤ j := by omega
-    simp [t]
-
-theorem getElem_insertIdx_loop {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {k : Nat} {h} :
-    (insertIdx.loop i as ⟨j, hj⟩)[k] =
-      if h₁ : k < i then
-        as[k]'(by simpa using h)
-      else
-        if h₂ : k = i then
-          if i ≤ j then as[j] else as[i]'(by simpa [h₂] using h)
-        else
-          if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
-  split <;> rename_i h₁
-  · rw [getElem_insertIdx_loop_lt h₁]
-  · split <;> rename_i h₂
-    · subst h₂
-      rw [getElem_insertIdx_loop_eq]
-    · rw [getElem_insertIdx_loop_gt (by omega)]
-
-theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
-    (k) (h' : k < (as.insertIdx i v).size) :
-    (as.insertIdx i v)[k] =
-      if h₁ : k < i then
-        as[k]'(by omega)
-      else
-        if h₂ : k = i then
-          v
-        else
-          as[k - 1]'(by simp at h'; omega) := by
-  unfold insertIdx
-  rw [getElem_insertIdx_loop]
-  simp only [size_insertIdx] at h'
-  replace h' : k ≤ as.size := by omega
-  simp only [getElem_push, h, ↓reduceIte, Nat.lt_irrefl, ↓reduceDIte, h', dite_eq_ite]
-  split <;> rename_i h₁
-  · rw [dif_pos (by omega)]
-  · split <;> rename_i h₂
-    · simp [h₂]
-    · split <;> rename_i h₃
-      · rfl
-      · omega
-
-theorem getElem_insertIdx_lt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
-    (k) (h' : k < (as.insertIdx i v).size) (h : k < i) :
-    (as.insertIdx i v)[k] = as[k] := by
-  simp [getElem_insertIdx, h]
-
-@[deprecated getElem_insertIdx_lt (since := "2024-11-20")] alias getElem_insertAt_lt :=
-getElem_insertIdx_lt
-
-theorem getElem_insertIdx_eq (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
-    (as.insertIdx i v)[i]'(by simp; omega) = v := by
-  simp [getElem_insertIdx, h]
-
-@[deprecated getElem_insertIdx_eq (since := "2024-11-20")] alias getElem_insertAt_eq :=
-getElem_insertIdx_eq
-
-theorem getElem_insertIdx_gt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
-    (k) (h' : k < (as.insertIdx i v).size) (h : i < k) :
-    (as.insertIdx i v)[k] = as[k-1]'(by simp at h'; omega) := by
-  rw [getElem_insertIdx]
-  rw [dif_neg (by omega), dif_neg (by omega)]
-
-@[deprecated getElem_insertIdx_gt (since := "2024-11-20")] alias getElem_insertAt_gt :=
-getElem_insertIdx_gt
+@[deprecated (since := "2024-11-20")] alias size_insertAt := size_insertIdx
+@[deprecated (since := "2024-11-20")] alias getElem_insertAt_lt := getElem_insertIdx_of_lt
+@[deprecated (since := "2024-11-20")] alias getElem_insertAt_eq := getElem_insertIdx_self
+@[deprecated (since := "2024-11-20")] alias getElem_insertAt_gt := getElem_insertIdx_of_gt
+
+@[deprecated (since := "2025-02-06")] alias getElem_insertIdx_lt := getElem_insertIdx_of_lt
+@[deprecated (since := "2025-02-06")] alias getElem_insertIdx_eq := getElem_insertIdx_self
+@[deprecated (since := "2025-02-06")] alias getElem_insertIdx_gt := getElem_insertIdx_of_gt
diff --git a/Batteries/Data/Array/Monadic.lean b/Batteries/Data/Array/Monadic.lean
@@ -182,122 +182,3 @@ theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α
   · exact .pure rfl
 
 end Array
-
-namespace List
-
-theorem filterM_toArray [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) :
-    l.toArray.filterM p = toArray <$> l.filterM p := by
-  simp only [Array.filterM, filterM, foldlM_toArray, bind_pure_comp, Functor.map_map]
-  conv => lhs; rw [← reverse_nil]
-  generalize [] = acc
-  induction l generalizing acc with simp
-  | cons x xs ih =>
-    congr; funext b
-    cases b
-    · simp only [Bool.false_eq_true, ↓reduceIte, pure_bind, cond_false]
-      exact ih acc
-    · simp only [↓reduceIte, ← reverse_cons, pure_bind, cond_true]
-      exact ih (x :: acc)
-
-theorem filterRevM_toArray [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) :
-    l.toArray.filterRevM p = toArray <$> l.filterRevM p := by
-  simp [Array.filterRevM, filterRevM]
-  rw [← foldlM_reverse, ← foldlM_toArray, ← Array.filterM, filterM_toArray]
-  simp only [filterM, bind_pure_comp, Functor.map_map, reverse_toArray, reverse_reverse]
-
-theorem filterMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Option β)) :
-    l.toArray.filterMapM f = toArray <$> l.filterMapM f := by
-  simp [Array.filterMapM, filterMapM]
-  conv => lhs; rw [← reverse_nil]
-  generalize [] = acc
-  induction l generalizing acc with simp [filterMapM.loop]
-  | cons x xs ih =>
-    congr; funext o
-    cases o
-    · simp only [pure_bind]; exact ih acc
-    · simp only [pure_bind]; rw [← List.reverse_cons]; exact ih _
-
-theorem flatMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Array β)) :
-    l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a) := by
-  simp only [Array.flatMapM, bind_pure_comp, foldlM_toArray, flatMapM]
-  conv => lhs; arg 2; change [].reverse.flatten.toArray
-  generalize [] = acc
-  induction l generalizing acc with
-  | nil => simp only [foldlM_nil, flatMapM.loop, map_pure]
-  | cons x xs ih =>
-    simp only [foldlM_cons, bind_map_left, flatMapM.loop, _root_.map_bind]
-    congr; funext a
-    conv => lhs; rw [Array.toArray_append, ← flatten_concat, ← reverse_cons]
-    exact ih _
-
-theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
-    (f : (i : Nat) → α → (h : i < l.length) → m β) :
-    l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f := by
-  let rec go (i : Nat) (acc : Array β) (inv : i + acc.size = l.length) :
-      Array.mapFinIdxM.map l.toArray f i acc.size inv acc
-      = toArray <$> mapFinIdxM.go l f (l.drop acc.size) acc
-        (by simp [Nat.sub_add_cancel (Nat.le.intro (Nat.add_comm _ _ ▸ inv))]) := by
-    match i with
-    | 0 =>
-      rw [Nat.zero_add] at inv
-      simp only [Array.mapFinIdxM.map, inv, drop_length, mapFinIdxM.go, map_pure]
-    | k + 1 =>
-      conv => enter [2, 2, 3]; rw [← getElem_cons_drop l acc.size (by omega)]
-      simp only [Array.mapFinIdxM.map, mapFinIdxM.go, _root_.map_bind]
-      congr; funext x
-      conv => enter [1, 4]; rw [← Array.size_push _ x]
-      conv => enter [2, 2, 3]; rw [← Array.size_push _ x]
-      refine go k (acc.push x) _
-  simp only [Array.mapFinIdxM, mapFinIdxM]
-  exact go _ #[] _
-
-theorem mapIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
-    (f : Nat → α → m β) :
-    l.toArray.mapIdxM f = toArray <$> l.mapIdxM f := by
-  let rec go (bs : List α) (acc : Array β) (inv : bs.length + acc.size = l.length) :
-      mapFinIdxM.go l (fun i a h => f i a) bs acc inv = mapIdxM.go f bs acc := by
-    match bs with
-    | [] => simp only [mapFinIdxM.go, mapIdxM.go]
-    | x :: xs => simp only [mapFinIdxM.go, mapIdxM.go, go]
-  unfold Array.mapIdxM
-  rw [mapFinIdxM_toArray]
-  simp only [mapFinIdxM, mapIdxM]
-  rw [go]
-
-end List
-
-namespace Array
-
-theorem toList_filterM [Monad m] [LawfulMonad m] (a : Array α) (p : α → m Bool) :
-    toList <$> a.filterM p = a.toList.filterM p := by
-  rw [List.filterM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_filterRevM [Monad m] [LawfulMonad m] (a : Array α) (p : α → m Bool) :
-    toList <$> a.filterRevM p = a.toList.filterRevM p := by
-  rw [List.filterRevM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_filterMapM [Monad m] [LawfulMonad m] (a : Array α) (f : α → m (Option β)) :
-    toList <$> a.filterMapM f = a.toList.filterMapM f := by
-  rw [List.filterMapM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_flatMapM [Monad m] [LawfulMonad m] (a : Array α) (f : α → m (Array β)) :
-    toList <$> a.flatMapM f = a.toList.flatMapM (fun a => toList <$> f a) := by
-  rw [List.flatMapM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_mapFinIdxM [Monad m] [LawfulMonad m] (l : Array α)
-    (f : (i : Nat) → α → (h : i < l.size) → m β) :
-    toList <$> l.mapFinIdxM f = l.toList.mapFinIdxM f := by
-  rw [List.mapFinIdxM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_mapIdxM [Monad m] [LawfulMonad m] (l : Array α)
-    (f : Nat → α → m β) :
-    toList <$> l.mapIdxM f = l.toList.mapIdxM f := by
-  rw [List.mapIdxM_toArray]
-  simp only [Functor.map_map, id_map']
-
-end Array
diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean
@@ -19,14 +19,12 @@ that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is
 -/
 def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R
 
-theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
-    ∀ (i j : Fin as.size), i < j → R (as.get i i.2) (as.get j j.2) := by
-  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_getElem_toList]
-
 theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Nat) (_ : i < as.size) (_ : j < as.size), i < j → R as[i] as[j] := by
   unfold Pairwise; simp [List.pairwise_iff_getElem, length_toList]
 
+@[deprecated (since := "2025-02-19")] alias pairwise_iff_get := pairwise_iff_getElem
+
 instance (R : α → α → Prop) [DecidableRel R] (as) : Decidable (Pairwise R as) :=
   have : (∀ (j : Fin as.size) (i : Fin j.val), R as[i.val] (as[j.val])) ↔ Pairwise R as := by
     rw [pairwise_iff_getElem]