Update lean-toolchain for leanprover/lean4#10524

Author: leanprover-community-mathlib4-bot

Batteries.lean

@@ -24,7 +24,7 @@ import Batteries.Data.BinaryHeap
 import Batteries.Data.BinomialHeap
 import Batteries.Data.BitVec
 import Batteries.Data.ByteArray
-import Batteries.Data.ByteSubarray
+import Batteries.Data.ByteSlice
 import Batteries.Data.Char
 import Batteries.Data.DList
 import Batteries.Data.Fin

Batteries/Control/OptionT.lean

@@ -14,63 +14,12 @@ This file contains lemmas about the behavior of `OptionT` and `OptionT.run`.
 
 namespace OptionT
 
-@[ext] theorem ext {x x' : OptionT m α} (h : x.run = x'.run) : x = x' := h
-
-@[simp] theorem run_mk {m : Type _ → Type _} (x : m (Option α)) :
-    OptionT.run (OptionT.mk x) = x := rfl
-
-@[simp] theorem run_pure (a) [Monad m] : (pure a : OptionT m α).run = pure (some a) := rfl
-
-@[simp] theorem run_bind (f : α → OptionT m β) [Monad m] :
-    (x >>= f).run = Option.elimM x.run (pure none) (run ∘ f) := by
-  change x.run >>= _ = _
-  simp [Option.elimM]
-  exact bind_congr fun |some _ => rfl | none => rfl
-
-@[simp] theorem run_map (x : OptionT m α) (f : α → β) [Monad m] [LawfulMonad m] :
-    (f <$> x).run = Option.map f <$> x.run := by
-  rw [← bind_pure_comp _ x.run]
-  change x.run >>= _ = _
-  exact bind_congr fun |some _ => rfl | none => rfl
-
 @[simp] theorem run_monadLift [Monad m] [LawfulMonad m] [MonadLiftT n m] (x : n α) :
     (monadLift x : OptionT m α).run = some <$> (monadLift x : m α) := (map_eq_pure_bind _ _).symm
 
 @[simp] theorem run_mapConst [Monad m] [LawfulMonad m] (x : OptionT m α) (y : β) :
     (Functor.mapConst y x).run = Option.map (Function.const α y) <$> x.run := run_map _ _
 
-instance (m) [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) :=
-  LawfulMonad.mk'
-    (id_map := by
-      intros; apply OptionT.ext; simp only [OptionT.run_map]
-      rw [map_congr, id_map]
-      intro a; cases a <;> rfl)
-    (bind_assoc := by
-      refine fun _ _ _ => OptionT.ext ?_
-      simp only [run_bind, Option.elimM, bind_assoc]
-      refine bind_congr fun | some x => by simp [Option.elimM] | none => by simp)
-    (pure_bind := by intros; apply OptionT.ext; simp)
-
-@[simp] theorem run_failure [Monad m] : (failure : OptionT m α).run = pure none := rfl
-
-@[simp] theorem run_orElse [Monad m] (x : OptionT m α) (y : OptionT m α) :
-    (x <|> y).run = Option.elimM x.run y.run (pure ∘ some) :=
-  bind_congr fun | some _ => rfl | none => rfl
-
-@[simp] theorem run_seq [Monad m] [LawfulMonad m] (f : OptionT m (α → β)) (x : OptionT m α) :
-    (f <*> x).run = Option.elimM f.run (pure none) (fun f => Option.map f <$> x.run) := by
-  simp only [seq_eq_bind, run_bind, run_map, Function.comp_def]
-
-@[simp] theorem run_seqLeft [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
-    (x <* y).run = Option.elimM x.run (pure none)
-      (fun x => Option.map (Function.const β x) <$> y.run) := by
-  simp [seqLeft_eq, seq_eq_bind, Option.elimM, Function.comp_def]
-
-@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
-    (x *> y).run = Option.elimM x.run (pure none) (Function.const α y.run) := by
-  simp only [seqRight_eq, run_seq, run_map, Option.elimM_map]
-  refine bind_congr (fun | some _ => by simp [Option.elim] | none => by simp [Option.elim])
-
 @[simp] theorem run_monadMap {n} [MonadFunctorT n m] (f : ∀ {α}, n α → n α) :
     (monadMap (@f) x : OptionT m α).run = monadMap (@f) x.run := rfl
 

Batteries/Data/Array/Match.lean

@@ -61,7 +61,7 @@ def PrefixTable.extend [BEq α] (t : PrefixTable α) (x : α) : PrefixTable α w
 def mkPrefixTable [BEq α] (xs : Array α) : PrefixTable α := xs.foldl (·.extend) default
 
 /-- Make prefix table from a pattern stream -/
-partial def mkPrefixTableOfStream [BEq α] [Stream σ α] (stream : σ) : PrefixTable α :=
+partial def mkPrefixTableOfStream [BEq α] [Std.Stream σ α] (stream : σ) : PrefixTable α :=
   loop default stream
 where
   /-- Inner loop for `mkPrefixTableOfStream` -/
@@ -82,15 +82,15 @@ def Matcher.ofArray [BEq α] (pat : Array α) : Matcher α where
   table := mkPrefixTable pat
 
 /-- Make a KMP matcher for a given a pattern stream -/
-def Matcher.ofStream [BEq α] [Stream σ α] (pat : σ) : Matcher α where
+def Matcher.ofStream [BEq α] [Std.Stream σ α] (pat : σ) : Matcher α where
   table := mkPrefixTableOfStream pat
 
 /-- Find next match from a given stream
 
   Runs the stream until it reads a sequence that matches the sought pattern, then returns the stream
   state at that point and an updated matcher state.
 -/
-partial def Matcher.next? [BEq α] [Stream σ α] (m : Matcher α) (stream : σ) :
+partial def Matcher.next? [BEq α] [Std.Stream σ α] (m : Matcher α) (stream : σ) :
     Option (σ × Matcher α) :=
   match Stream.next? stream with
   | none => none

Batteries/Data/Array/Monadic.lean

@@ -16,8 +16,8 @@ in order to minimize dependence on `SatisfiesM`.
 
 namespace Array
 
-theorem SatisfiesM_foldlM [Monad m] [LawfulMonad m]
-    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → m β}
+theorem SatisfiesM_foldlM [Monad m] [LawfulMonad m] {as : Array α} {init : β}
+    {motive : Nat → β → Prop} {f : β → α → m β} (h0 : motive 0 init)
     (hf : ∀ i : Fin as.size, ∀ b, motive i.1 b → SatisfiesM (motive (i.1 + 1)) (f b as[i])) :
     SatisfiesM (motive as.size) (as.foldlM f init) := by
   let rec go {i j b} (h₁ : j ≤ as.size) (h₂ : as.size ≤ i + j) (H : motive j b) :
@@ -30,9 +30,8 @@ theorem SatisfiesM_foldlM [Monad m] [LawfulMonad m]
     · next hj => exact Nat.le_antisymm h₁ (Nat.ge_of_not_lt hj) ▸ .pure H
   simp [foldlM]; exact go (Nat.zero_le _) (Nat.le_refl _) h0
 
-theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β)
-    (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin as.size → β → Prop)
+theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] {as : Array α} {f : α → m β}
+    {motive : Nat → Prop} {p : Fin as.size → β → Prop} (h0 : motive 0)
     (hs : ∀ i, motive i.1 → SatisfiesM (p i · ∧ motive (i + 1)) (f as[i])) :
     SatisfiesM
       (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
@@ -48,26 +47,19 @@ theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m
     simp [getElem_push] at hj ⊢; split; {apply ih₂}
     cases j; cases (Nat.le_or_eq_of_le_succ hj).resolve_left ‹_›; cases eq; exact h₁
 
-theorem SatisfiesM_mapM' [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β)
-    (p : Fin as.size → β → Prop)
+theorem SatisfiesM_mapM' [Monad m] [LawfulMonad m] {as : Array α} {f : α → m β}
+    {p : Fin as.size → β → Prop}
     (hs : ∀ i, SatisfiesM (p i) (f as[i])) :
     SatisfiesM
       (fun arr => ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
       (Array.mapM f as) :=
-  (SatisfiesM_mapM _ _ (fun _ => True) trivial _ (fun _ h => (hs _).imp (⟨·, h⟩))).imp (·.2)
+  (SatisfiesM_mapM (motive := fun _ => True) trivial (fun _ h => (hs _).imp (⟨·, h⟩))).imp (·.2)
 
 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)
+  (SatisfiesM_mapM' (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)
+theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α}
     (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 →
       SatisfiesM (bif · then tru else fal (i + 1)) (p as[i])) :
@@ -91,14 +83,14 @@ theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Arra
   exact go hstart _ h0 fun i hi => hp i <| Nat.lt_of_lt_of_le hi <| Nat.min_le_left ..
 
 theorem SatisfiesM_anyM_iff_exists [Monad m] [LawfulMonad m]
-    (p : α → m Bool) (as : Array α) (start stop) (q : Fin as.size → Prop)
+    {p : α → m Bool} {as : Array α} {q : Fin as.size → Prop}
     (hp : ∀ i : Fin as.size, start ≤ i.1 → i.1 < stop → SatisfiesM (· = true ↔ q i) (p as[i])) :
     SatisfiesM
       (fun res => res = true ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ q i)
       (anyM p as start stop) := by
   cases Nat.le_total start (min stop as.size) with
   | inl hstart =>
-    refine (SatisfiesM_anyM _ _ _ _ hstart
+    refine (SatisfiesM_anyM hstart
       (fal := fun j => start ≤ j ∧ ¬ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < j ∧ q i)
       (tru := ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ q i) ?_ ?_).imp ?_
     · exact ⟨Nat.le_refl _, fun ⟨i, h₁, h₂, _⟩ => (Nat.not_le_of_gt h₂ h₁).elim⟩
@@ -118,8 +110,8 @@ theorem SatisfiesM_anyM_iff_exists [Monad m] [LawfulMonad m]
     cases Nat.not_lt.2 (Nat.le_trans hstart h₁) (Nat.lt_min.2 ⟨h₂, j.2⟩)
 
 theorem SatisfiesM_foldrM [Monad m] [LawfulMonad m]
-    {as : Array α} (motive : Nat → β → Prop)
-    {init : β} (h0 : motive as.size init) {f : α → β → m β}
+    {as : Array α} {init : β} {motive : Nat → β → Prop} {f : α → β → m β}
+    (h0 : motive as.size init)
     (hf : ∀ i : Fin as.size, ∀ b, motive (i.1 + 1) b → SatisfiesM (motive i.1) (f as[i] b)) :
     SatisfiesM (motive 0) (as.foldrM f init) := by
   let rec go {i b} (hi : i ≤ as.size) (H : motive i b) :
@@ -133,11 +125,10 @@ 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 : (i : Nat) → α → (h : i < as.size) → m β)
-    (motive : Nat → Prop) (h0 : motive 0)
-    (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)) :
+theorem SatisfiesM_mapFinIdxM [Monad m] [LawfulMonad m]
+    {as : Array α} {f : (i : Nat) → α → i < as.size → m β} {motive : Nat → Prop}
+    {p : (i : Nat) → β → i < as.size → Prop}
+    (h0 : motive 0) (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 arr[i] h)
       (Array.mapFinIdxM as f) := by
@@ -156,27 +147,26 @@ theorem SatisfiesM_mapFinIdxM [Monad m] [LawfulMonad m] (as : Array α)
       · 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 : (i : Nat) → β → (h : i < as.size) → Prop)
-    (hs : ∀ i h, motive i → SatisfiesM (p i · h ∧ motive (i + 1)) (f i as[i])) :
+theorem SatisfiesM_mapIdxM [Monad m] [LawfulMonad m] {as : Array α} {f : Nat → α → m β}
+    {p : (i : Nat) → β → i < as.size → Prop} {motive : Nat → Prop}
+    (h0 : motive 0) (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 arr[i] h)
       (as.mapIdxM f) :=
-  SatisfiesM_mapFinIdxM as (fun i a _ => f i a) motive h0 p hs
+  SatisfiesM_mapFinIdxM h0 hs
 
 theorem size_mapFinIdxM [Monad m] [LawfulMonad m]
-    (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → m β) :
+    (as : Array α) (f : (i : Nat) → α → i < as.size → m β) :
     SatisfiesM (fun arr => arr.size = as.size) (Array.mapFinIdxM as f) :=
-  (SatisfiesM_mapFinIdxM _ _ (fun _ => True) trivial (fun _ _ _ => True)
+  (SatisfiesM_mapFinIdxM (motive := fun _ => True) trivial
     (fun _ _ _ => .of_true fun _ => ⟨trivial, trivial⟩)).imp (·.2.1)
 
 theorem size_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Nat → α → m β) :
     SatisfiesM (fun arr => arr.size = as.size) (Array.mapIdxM f as) :=
   size_mapFinIdxM _ _
 
-theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α → m α) :
-    SatisfiesM (·.size = a.size) (a.modifyM i f) := by
+theorem size_modifyM [Monad m] [LawfulMonad m] (as : Array α) (i : Nat) (f : α → m α) :
+    SatisfiesM (·.size = as.size) (as.modifyM i f) := by
   unfold modifyM; split
   · exact .bind_pre <| .of_true fun _ => .pure <| by simp only [size_set]
   · exact .pure rfl

Batteries/Data/AssocList.lean

@@ -252,8 +252,8 @@ def pop? : AssocList α β → Option ((α × β) × AssocList α β)
   | nil => none
   | cons a b l => some ((a, b), l)
 
-instance : ToStream (AssocList α β) (AssocList α β) := ⟨fun x => x⟩
-instance : Stream (AssocList α β) (α × β) := ⟨pop?⟩
+instance : Std.ToStream (AssocList α β) (AssocList α β) := ⟨fun x => x⟩
+instance : Std.Stream (AssocList α β) (α × β) := ⟨pop?⟩
 
 /-- Converts a list into an `AssocList`. This is the inverse function to `AssocList.toList`. -/
 @[simp] def _root_.List.toAssocList : List (α × β) → AssocList α β

Batteries/Data/BinomialHeap/Basic.lean

@@ -532,7 +532,7 @@ def ofArray (le : α → α → Bool) (as : Array α) : BinomialHeap α le := as
   | none => none
   | some (a, tl) => some (a, ⟨tl, b.2.deleteMin eq⟩)
 
-instance : Stream (BinomialHeap α le) α := ⟨deleteMin⟩
+instance : Std.Stream (BinomialHeap α le) α := ⟨deleteMin⟩
 
 /--
 `O(n log n)`. Implementation of `for x in (b : BinomialHeap α le) ...` notation,