Update lean-toolchain for leanprover/lean4#12481

Author: leanprover-community-mathlib4-bot

.github/workflows/nightly_bump_toolchain.yml

@@ -29,8 +29,15 @@ jobs:
 
     - name: Get latest release tag from leanprover/lean4-nightly
       id: get-latest-release
+      env:
+        GH_TOKEN: ${{ steps.app-token.outputs.token }}
       run: |
-        RELEASE_TAG=$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')
+        RELEASE_TAG=$(gh api -X GET repos/leanprover/lean4-nightly/releases \
+          -f per_page=1 --jq '.[0].tag_name')
+        if [ -z "$RELEASE_TAG" ] || [ "$RELEASE_TAG" = "null" ]; then
+          echo "::error::Could not determine latest lean4-nightly release"
+          exit 1
+        fi
         echo "RELEASE_TAG=$RELEASE_TAG" >> $GITHUB_ENV
 
     - name: Update lean-toolchain file

.github/workflows/test_mathlib.yml

@@ -59,7 +59,7 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: Check if tag exists
+      - name: Check if branch exists
         if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
         id: check_mathlib_tag
         env:
@@ -75,7 +75,7 @@ jobs:
           BASE=master
           echo "Using base tag: $BASE"
 
-          EXISTS="$(git ls-remote --heads origin batteries-pr-testing-$PR_NUMBER | wc -l)"
+          EXISTS="$(git ls-remote --heads nightly-testing batteries-pr-testing-$PR_NUMBER | wc -l)"
           echo "Branch exists: $EXISTS"
           if [ "$EXISTS" = "0" ]; then
             echo "Branch does not exist, creating it."

Batteries/Classes/SatisfiesM.lean

@@ -193,8 +193,8 @@ theorem SatisfiesM_ReaderT_eq [Monad m] :
   (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm
 
 theorem SatisfiesM_StateRefT_eq [Monad m] :
-    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by
-  simp [SatisfiesM_ReaderT_eq, ReaderT.run]
+    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) :=
+  SatisfiesM_ReaderT_eq
 
 theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s) := by

Batteries/Control/AlternativeMonad.lean

@@ -197,9 +197,9 @@ instance [AlternativeMonad m] : AlternativeMonad (StateRefT' ω σ m) where
 
 instance [AlternativeMonad m] [LawfulAlternative m] :
     LawfulAlternative (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulAlternative (ReaderT _ _))
+  inferInstanceAs (LawfulAlternative (ReaderT (ST.Ref ω σ) m))
 
 instance [AlternativeMonad m] : LawfulAlternativeLift m (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulAlternativeLift m (ReaderT _ _))
+  inferInstanceAs (LawfulAlternativeLift m (ReaderT (ST.Ref ω σ) m))
 
 end StateRefT'

Batteries/Control/LawfulMonadState.lean

@@ -222,4 +222,4 @@ instance {m σ ρ} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadSta
 
 instance {m ω σ} [Monad m] [LawfulMonad m] [MonadStateOf σ m] [LawfulMonadStateOf σ m] :
     LawfulMonadStateOf σ (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulMonadStateOf σ (ReaderT _ _))
+  inferInstanceAs (LawfulMonadStateOf σ (ReaderT (ST.Ref ω σ) m))

Batteries/Data/Array/Basic.lean

@@ -5,6 +5,7 @@ Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg
 -/
 module
 import Batteries.Tactic.Alias
+import Batteries.Data.UInt
 
 @[expose] public section
 
@@ -140,12 +141,6 @@ May be asserted to be true in an unsafe context via `Array.unsafe_sizeFitsUsize`
 -/
 private abbrev SizeFitsUSize (a : Array α) : Prop := a.size < USize.size
 
-@[grind .]
-private theorem SizeFitsUSize.toNat_ofNat_eq {n : Nat} {a : Array α}
-    (h : a.SizeFitsUSize) (hn : n ≤ a.size) :
-    (USize.ofNat n).toNat = n :=
-  USize.toNat_ofNat_of_lt' (Nat.lt_of_le_of_lt ‹_› ‹_›)
-
 /-
 This is guaranteed by the Array docs but it is unprovable.
 Can be used in unsafe functions to write more efficient implementations
@@ -224,13 +219,13 @@ private theorem scanlM_loop_eq_scanlMFast_loop [Monad m]
     {h_stop : stop ≤ as.size} {acc : Array β} :
     scanlM.loop f init as start stop h_stop acc
       = scanlMFast.loop f init as (USize.ofNat start) (USize.ofNat stop)
-      (by rw [USize.toNat_ofNat_of_lt' (Nat.lt_of_le_of_lt h_stop h_size)]; exact h_stop) acc := by
+      (by rw [USize.toNat_ofNat_of_le_of_lt h_size h_stop]; exact h_stop) acc := by
   generalize h_n : stop - start = n
   induction n using Nat.strongRecOn generalizing start acc init
   rename_i n ih
   rw [scanlM.loop, scanlMFast.loop]
-  have h_stop_usize := h_size.toNat_ofNat_eq h_stop
-  have h_start_usize := h_size.toNat_ofNat_eq h_start
+  have h_stop_usize := USize.toNat_ofNat_of_le_of_lt h_size h_stop
+  have h_start_usize := USize.toNat_ofNat_of_le_of_lt h_size h_start
   split
   case isTrue h_lt =>
     simp_all only [USize.toNat_ofNat', ↓reduceDIte, uget,
@@ -239,7 +234,7 @@ private theorem scanlM_loop_eq_scanlMFast_loop [Monad m]
     intro next
     have h_start_succ : USize.ofNat start + 1 = USize.ofNat (start + 1) := by
       simp_all only [← USize.toNat_inj, USize.toNat_add]
-      grind only [USize.size_eq, SizeFitsUSize.toNat_ofNat_eq]
+      grind only [USize.size_eq, USize.toNat_ofNat_of_le_of_lt]
     rw [h_start_succ]
     apply ih (stop - (start + 1)) <;> omega
   case isFalse h_nlt => grind [USize.lt_iff_toNat_lt]
@@ -265,7 +260,7 @@ private def scanrMFast [Monad m] (f : α → β → m β) (init : β) (as : Arra
     (start := USize.ofNat start) (stop := USize.ofNat stop)
     (h_start := by grind only [USize.size_eq, USize.ofNat_eq_iff_mod_eq_toNat, = Nat.min_def])
     (acc := Array.replicate (start - stop + 1) init)
-    (by grind only [!Array.size_replicate, = Nat.min_def, SizeFitsUSize.toNat_ofNat_eq])
+    (by grind only [!Array.size_replicate, = Nat.min_def, USize.toNat_ofNat_of_le_of_lt])
 where
   @[specialize]
   loop (f : α → β → m β) (init : β) (as : Array α)

Batteries/Data/Array/Scan.lean

@@ -19,6 +19,7 @@ Prove basic results about `Array.scanl`, `Array.scanr`, `Array.scanlM` and `Arra
 -/
 namespace Array
 
+set_option backward.isDefEq.respectTransparency false in
 theorem scanlM.loop_toList [Monad m] [LawfulMonad m]
     {f : β → α → m β} {stop : Nat} (h : stop ≤ as.size) :
     Array.toList <$> scanlM.loop f init as start stop h acc =
@@ -152,7 +153,8 @@ theorem scanl_eq_scanlM {f : β → α → β} {as: Array α} :
 
 theorem scanl_eq_scanl_toList {f: β → α → β} {as : Array α} :
     as.scanl f init = (as.toList.scanl f init).toArray := by
-  simp only [scanl_eq_scanlM, scanlM_eq_scanlM_toList, List.scanl, pure, Id.run_map]
+  simp only [scanl_eq_scanlM, scanlM_eq_scanlM_toList]
+  simp [List.idRun_scanlM]
 
 @[simp, grind =]
 theorem toList_scanl {f : β → α → β} {as: Array α} :
@@ -244,7 +246,7 @@ theorem scanr_eq_scanrM {f : α → β → β} {as : Array α} :
 theorem scanr_eq_scanr_toList {f : α → β → β} {as : Array α} :
     as.scanr f init = (as.toList.scanr f init).toArray := by
   simp only [scanr_eq_scanrM, scanrM_eq_scanrM_toList]
-  simp [List.scanr]
+  simp [List.idRun_scanrM]
 
 @[simp, grind =]
 theorem toList_scanr {f : α → β → β} {as : Array α} :

Batteries/Data/ByteArray.lean

@@ -78,7 +78,7 @@ theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start s
 
 @[simp] theorem get_extract {a : ByteArray} {start stop} (h : i < (a.extract start stop).size) :
     (a.extract start stop)[i] = a[start+i]'(get_extract_aux h) := by
-  simp [getElem_eq_data_getElem]
+  simp [getElem_eq_data_getElem]; rfl
 
 /-! ### ofFn -/
 

Batteries/Data/Fin/Fold.lean

@@ -20,6 +20,8 @@ theorem dfoldrM_loop_zero [Monad m] (f : (i : Fin n) → α i.succ → m (α i.c
 theorem dfoldrM_loop_succ [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x) :
     dfoldrM.loop n α f (i+1) h x = f ⟨i, by omega⟩ x >>= dfoldrM.loop n α f i (by omega) := rfl
 
+-- TODO: This proof needs adjustment for lean4#12179 (backward.isDefEq.respectTransparency)
+set_option backward.isDefEq.respectTransparency false in
 theorem dfoldrM_loop [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc))
     (x) : dfoldrM.loop (n+1) α f (i+1) h x =
       dfoldrM.loop n (α ∘ succ) (f ·.succ) i (by omega) x >>= f 0 := by
@@ -77,7 +79,7 @@ theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α
 
 theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) :
     dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by
-  rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq]
+  rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _)]; rfl
 
 @[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) :
     dfoldlM 0 α f x = pure x := by simp [dfoldlM, dfoldlM.loop]
@@ -93,7 +95,7 @@ theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α
     cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
     rw [dfoldlM_loop_lt _ h]
     congr; funext
-    rw [dfoldlM_loop_eq, dfoldlM_loop_eq]
+    rw [dfoldlM_loop_eq, dfoldlM_loop_eq]; rfl
 
 theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x) :
     dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) :=

Batteries/Data/List/Basic.lean

@@ -194,42 +194,6 @@ where
     | [], last, acc => pure <| last :: acc
     | x :: xs, last, acc => do go xs (← f last x) (last :: acc)
 
-/--
-Folds a monadic function over a list from the left, accumulating partial results starting with
-`init`. The accumulated values are combined with the each element of the list in order, using `f`.
--/
-@[inline]
-def scanlM [Monad m] (f : β → α → m β) (init : β) (l : List α) : m (List β) :=
-  List.reverse <$> scanAuxM f init l
-
-/--
-Folds a monadic function over a list from the right, accumulating partial results starting with
-`init`. The accumulated values are combined with the each element of the list in order, using `f`.
--/
-@[inline]
-def scanrM [Monad m] (f : α → β → m β) (init : β) (xs : List α) : m (List β) :=
-  scanAuxM (flip f) init xs.reverse
-
-/--
-Fold a function `f` over the list from the left, returning the list of partial results.
-```
-scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]
-```
--/
-@[inline]
-def scanl (f : β → α → β) (init : β) (as : List α) : List β :=
-  Id.run <| as.scanlM (pure <| f · ·) init
-
-/--
-Fold a function `f` over the list from the right, returning the list of partial results.
-```
-scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]
-```
--/
-@[inline]
-def scanr (f : α → β → β) (init : β) (as : List α) : List β :=
-  Id.run <| as.scanrM (pure <| f · ·) init
-
 /--
 Fold a list from left to right as with `foldl`, but the combining function
 also receives each element's index added to an optional parameter `start`