Update lean-toolchain for leanprover/lean4#9932

Author: leanprover-community-mathlib4-bot

Batteries/Classes/RatCast.lean

@@ -3,7 +3,6 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro, Gabriel Ebner
 -/
-import Batteries.Data.Rat.Basic
 
 /-- Type class for the canonical homomorphism `Rat → K`. -/
 class RatCast (K : Type u) where

Batteries/Control/Lemmas.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: François G. Dorais
+Authors: François G. Dorais, Eric Wieser
 -/
 
 namespace ReaderT
@@ -14,6 +14,21 @@ attribute [ext] ReaderT.ext
 @[simp] theorem run_orElse [Monad m] [Alternative m] (x y : ReaderT ρ m α) (ctx : ρ) :
     (x <|> y).run ctx = (x.run ctx <|> y.run ctx) := rfl
 
+@[simp] theorem run_throw [MonadExceptOf ε m] (e : ε) (ctx : ρ) :
+    (throw e : ReaderT ρ m α).run ctx = throw e := rfl
+
+@[simp] theorem run_throwThe [MonadExceptOf ε m] (e : ε) (ctx : ρ) :
+    (throwThe ε e : ReaderT ρ m α).run ctx = throwThe ε e := rfl
+
+@[simp] theorem run_tryCatch [MonadExceptOf ε m]
+    (body : ReaderT ρ m α) (handler : ε → ReaderT ρ m α) (ctx : ρ) :
+    (tryCatch body handler).run ctx = tryCatch (body.run ctx) (handler · |>.run ctx) := rfl
+
+@[simp] theorem run_tryCatchThe [MonadExceptOf ε m]
+    (body : ReaderT ρ m α) (handler : ε → ReaderT ρ m α) (ctx : ρ) :
+    (tryCatchThe ε body handler).run ctx = tryCatchThe ε (body.run ctx) (handler · |>.run ctx) :=
+  rfl
+
 end ReaderT
 
 namespace StateT
@@ -26,4 +41,18 @@ attribute [ext] StateT.ext
 @[simp] theorem run_orElse {α σ} [Monad m] [Alternative m] (x y : StateT σ m α) (s : σ) :
     (x <|> y).run s = (x.run s <|> y.run s) := rfl
 
+@[simp] theorem run_throw [Monad m] [MonadExceptOf ε m] (e : ε) (s : σ) :
+    (throw e : StateT σ m α).run s = (do let a ← throw e; pure (a, s)) := rfl
+
+@[simp] theorem run_throwThe [Monad m] [MonadExceptOf ε m] (e : ε) (s : σ) :
+    (throwThe ε e : StateT σ m α).run s = (do let a ← throwThe ε e; pure (a, s)) := rfl
+
+@[simp] theorem run_tryCatch [Monad m] [MonadExceptOf ε m]
+    (body : StateT σ m α) (handler : ε → StateT σ m α) (s : σ) :
+    (tryCatch body handler).run s = tryCatch (body.run s) (handler · |>.run s) := rfl
+
+@[simp] theorem run_tryCatchThe [Monad m] [MonadExceptOf ε m]
+    (body : StateT σ m α) (handler : ε → StateT σ m α) (s : σ) :
+    (tryCatchThe ε body handler).run s = tryCatchThe ε (body.run s) (handler · |>.run s) := rfl
+
 end StateT

Batteries/Control/Nondet/Basic.lean

@@ -50,8 +50,10 @@ structure Nondet (m : Type → Type) [MonadBacktrack σ m] (α : Type) : Type wh
   toMLList : MLList m (α × σ)
 
 namespace Nondet
+variable {m : Type → Type}
 
-variable {m : Type → Type} [Monad m] [MonadBacktrack σ m]
+section Monad
+variable [Monad m] [MonadBacktrack σ m]
 
 /-- The empty nondeterministic value. -/
 def nil : Nondet m α := .mk .nil
@@ -87,13 +89,10 @@ def singletonM (x : m α) : Nondet m α :=
 /-- Convert a value to the singleton nondeterministic value. -/
 def singleton (x : α) : Nondet m α := singletonM (pure x)
 
-/-- `Nondet m` is a monad. -/
-instance : Monad (Nondet m) where
+/-- `Nondet m` is an alternative monad. -/
+instance : AlternativeMonad (Nondet m) where
   pure a := singletonM (pure a)
   bind := bind
-
-/-- `Nondet m` is an alternative monad. -/
-instance : Alternative (Nondet m) where
   failure := .nil
   orElse x y := .mk <| x.toMLList.append fun _ => (y ()).toMLList
 
@@ -164,21 +163,6 @@ All iterations of a non-deterministic function on an initial value.
 partial def iterate (f : α → Nondet m α) (a : α) : Nondet m α :=
   singleton a <|> (f a).bind (iterate f)
 
-/--
-Find the first alternative in a nondeterministic value, as a monadic value.
--/
-def head [Alternative m] (L : Nondet m α) : m α := do
-  let (x, s) ← L.toMLList.head
-  restoreState s
-  return x
-
-/--
-Find the value of a monadic function on the first alternative in a nondeterministic value
-where the function succeeds.
--/
-def firstM [Alternative m] (L : Nondet m α) (f : α → m (Option β)) : m β :=
-  L.filterMapM f |>.head
-
 /--
 Convert a non-deterministic value into a lazy list, by discarding the backtrackable state.
 -/
@@ -194,6 +178,28 @@ Convert a non-deterministic value into a list in the monad, by discarding the ba
 -/
 def toList' (L : Nondet m α) : m (List α) := L.toMLList.map (·.1) |>.force
 
+end Monad
+
+section AlternativeMonad
+variable [AlternativeMonad m] [MonadBacktrack σ m]
+
+/--
+Find the first alternative in a nondeterministic value, as a monadic value.
+-/
+def head (L : Nondet m α) : m α := do
+  let (x, s) ← L.toMLList.head
+  restoreState s
+  return x
+
+/--
+Find the value of a monadic function on the first alternative in a nondeterministic value
+where the function succeeds.
+-/
+def firstM (L : Nondet m α) (f : α → m (Option β)) : m β :=
+  L.filterMapM f |>.head
+
+end AlternativeMonad
+
 end Nondet
 
 /-- The `Id` monad is trivially backtrackable, with state `Unit`. -/

Batteries/Data/Array/Match.lean

@@ -101,4 +101,66 @@ partial def Matcher.next? [BEq α] [Stream σ α] (m : Matcher α) (stream : σ)
     else
       next? { m with state } stream
 
+namespace Matcher
+open Std.Iterators
+
+/-- Iterator transformer for KMP matcher. -/
+protected structure Iterator (σ n α) [BEq α] (m : Matcher α) [Iterator σ n α] where
+  /-- Inner iterator. -/
+  inner : IterM (α := σ) n α
+  /-- Matcher state. -/
+  state : Fin (m.table.size + 1) := 0
+
+private def modifyStep [BEq α] (m : Matcher α) [Iterator σ n α]
+    (it : IterM (α := m.Iterator σ n α) n σ) :
+    it.internalState.inner.Step (α := σ) → IterStep (IterM (α := m.Iterator σ n α) n σ) σ
+  | .done _ => .done
+  | .skip it' _ => .skip ⟨{it.internalState with inner := it'}⟩
+  | .yield it' x _ =>
+    let state := m.table.step x m.state
+    if state = m.table.size then
+      .yield ⟨{inner := it', state := state}⟩ it'.internalState
+    else
+      .skip ⟨{inner := it', state := state}⟩
+
+instance [Monad n] [BEq α] (m : Matcher α) [Iterator σ n α] :
+    Iterator (m.Iterator σ n α) n σ where
+  IsPlausibleStep it step := ∃ step', m.modifyStep it step' = step
+  step it := it.internalState.inner.step >>= fun step => pure ⟨m.modifyStep _ _, step, rfl⟩
+
+private def finitenessRelation [Monad n] [BEq α] (m : Matcher α) [Iterator σ n α] [Finite σ n] :
+    FinitenessRelation (m.Iterator σ n α) n where
+  rel := InvImage IterM.IsPlausibleSuccessorOf fun it => it.internalState.inner
+  wf := InvImage.wf _ Finite.wf
+  subrelation {it it'} h := by
+    obtain ⟨_, hsucc, step, rfl⟩ := h
+    simp only [IterM.Step] at step
+    cases step with simp only [IterStep.successor, modifyStep, reduceCtorEq] at hsucc
+    | skip =>
+      cases hsucc
+      apply IterM.isPlausibleSuccessorOf_of_skip
+      assumption
+    | yield =>
+      split at hsucc
+      · next heq =>
+        cases hsucc
+        split at heq
+        · cases heq
+          apply IterM.isPlausibleSuccessorOf_of_yield
+          assumption
+        · contradiction
+      · next heq =>
+        cases hsucc
+        split at heq
+        · contradiction
+        · cases heq
+          apply IterM.isPlausibleSuccessorOf_of_yield
+          assumption
+      · contradiction
+
+instance [Monad n] [BEq α] (m : Matcher α) [Iterator σ n α] [inst : Finite σ n] :
+    Finite (m.Iterator σ n α) n (β := σ) := .of_finitenessRelation m.finitenessRelation
+
+end Matcher
+
 end Array

Batteries/Data/Array/Pairwise.lean

@@ -32,11 +32,11 @@ instance (R : α → α → Prop) [DecidableRel R] (as) : Decidable (Pairwise R
     · intro h ⟨j, hj⟩ ⟨i, hlt⟩; exact h i j (Nat.lt_trans hlt hj) hj hlt
   decidable_of_iff _ this
 
-@[grind]
+@[grind ←]
 theorem pairwise_empty : #[].Pairwise R := by
   unfold Pairwise; exact List.Pairwise.nil
 
-@[grind]
+@[grind ←]
 theorem pairwise_singleton (R : α → α → Prop) (a) : #[a].Pairwise R := by
   unfold Pairwise; exact List.pairwise_singleton ..
 

Batteries/Data/BitVec/Lemmas.lean

@@ -36,7 +36,7 @@ namespace BitVec
   simp only [BitVec.toInt, Int.ofBits, toNat_ofFnLE, Int.subNatNat_eq_coe]; rfl
 
 -- TODO: consider these for global `grind` attributes.
-attribute [local grind] Fin.succ Fin.rev Fin.last Fin.zero_eta
+attribute [local grind =] Fin.succ Fin.rev Fin.last Fin.zero_eta
 
 theorem getElem_ofFnLEAux (f : Fin n → Bool) (i) (h : i < n) (h' : i < m) :
     (ofFnLEAux m f)[i] = f ⟨i, h⟩ := by

Batteries/Data/ByteArray.lean

@@ -22,14 +22,8 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
 
 @[simp] theorem data_mkEmpty (cap) : (emptyWithCapacity cap).data = #[] := rfl
 
-@[simp] theorem data_empty : empty.data = #[] := rfl
-
-@[simp] theorem size_empty : empty.size = 0 := rfl
-
 /-! ### push -/
 
-@[simp] theorem data_push (a : ByteArray) (b : UInt8) : (a.push b).data = a.data.push b := rfl
-
 @[simp] theorem size_push (a : ByteArray) (b : UInt8) : (a.push b).size = a.size + 1 :=
   Array.size_push ..
 
@@ -68,15 +62,6 @@ theorem set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) :
 
 /-! ### append -/
 
-@[simp] theorem append_eq (a b) : ByteArray.append a b = a ++ b := rfl
-
-@[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_empty]
-
-theorem size_append (a b : ByteArray) : (a ++ b).size = a.size + b.size := by
-  simp only [size, append_eq, data_append]; exact Array.size_append ..
-
 theorem get_append_left {a b : ByteArray} (hlt : i < a.size)
     (h : i < (a ++ b).size := size_append .. ▸ Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)) :
     (a ++ b)[i] = a[i] := by
@@ -89,17 +74,6 @@ theorem get_append_right {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b
 
 /-! ### extract -/
 
-@[simp] theorem data_extract (a : ByteArray) (start stop) :
-    (a.extract start stop).data = a.data.extract start stop := by
-  simp [extract]
-  match Nat.le_total start stop with
-  | .inl h => simp [h, Nat.add_sub_cancel']
-  | .inr h => simp [h, Nat.sub_eq_zero_of_le, Array.extract_empty_of_stop_le_start]
-
-@[simp] theorem size_extract (a : ByteArray) (start stop) :
-    (a.extract start stop).size = min stop a.size - start := by
-  simp [size]
-
 theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start stop).size) :
     start + i < a.size := by
   apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h

Batteries/Data/Char/AsciiCasing.lean

@@ -5,7 +5,6 @@ Authors: François G. Dorais
 -/
 import Batteries.Data.Char.Basic
 import Batteries.Tactic.Basic
-import Std.Classes.Ord.String
 
 /-! # Lemmas for ASCII-casing