chore: merge main

.github/workflows/test_mathlib.yml

@@ -15,20 +15,16 @@ jobs:
       - name: Checkout PR
         uses: actions/checkout@v4
         with:
-          repository: ${{ github.event.workflow_run.head_repository.full_name }}
-          ref: ${{github.event.workflow_run.head_branch }}
           fetch-depth: 0
 
       - name: Get PR info
         id: pr-info
         run: |
-          echo "pullRequestNumber=$(gh pr view --json number -q .number || echo '')" >> $GITHUB_OUTPUT
-          echo "targetBranch=$(gh pr view --json baseRefName -q .baseRefName || echo '')" >> $GITHUB_OUTPUT
-          echo "HEAD_BRANCH=$(gh pr view --json headRefName -q .headRefName || echo '')" >> $GITHUB_ENV
-          echo "HEAD_REPO=$(gh pr view --json headRepository -q .headRepository.name || echo '')" >> $GITHUB_ENV
-          echo "HEAD_OWNER=$(gh pr view --json headRepositoryOwner -q .headRepositoryOwner.login || echo '')" >> $GITHUB_ENV
+          echo "pullRequestNumber=$(gh pr list --search $SHA --json number -q '.[0].number' || echo '')" >> $GITHUB_OUTPUT
+          echo "targetBranch=$(gh pr list --search $SHA --json baseRefName -q '.[0].baseRefName' || echo '')" >> $GITHUB_OUTPUT
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          SHA: ${{ github.event.workflow_run.head_sha }}
 
       - name: Checkout mathlib4 repository
         if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
@@ -52,14 +48,13 @@ jobs:
         id: check_mathlib_tag
         env:
           PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
-          HEAD_OWNER: ${{ env.HEAD_OWNER }}
-          HEAD_REPO: ${{ env.HEAD_REPO }}
-          HEAD_BRANCH: ${{ env.HEAD_BRANCH }}
+          HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }}
+          HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "[email protected]"
 
-          echo "PR info: $HEAD_OWNER $HEAD_REPO $HEAD_BRANCH"
+          echo "PR info: $HEAD_REPO $HEAD_BRANCH"
 
           BASE=master
           echo "Using base tag: $BASE"

Batteries.lean

@@ -34,7 +34,6 @@ import Batteries.Data.Range
 import Batteries.Data.Rat
 import Batteries.Data.Stream
 import Batteries.Data.String
-import Batteries.Data.Sum
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
 import Batteries.Data.Vector
@@ -73,7 +72,6 @@ import Batteries.StdDeprecations
 import Batteries.Tactic.Alias
 import Batteries.Tactic.Basic
 import Batteries.Tactic.Case
-import Batteries.Tactic.Classical
 import Batteries.Tactic.Congr
 import Batteries.Tactic.Exact
 import Batteries.Tactic.HelpCmd

Batteries/Data/Array/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg
 -/
 import Batteries.Data.Array.Init.Lemmas
+import Batteries.Tactic.Alias
 
 /-!
 ## Definitions on Arrays
@@ -14,10 +15,6 @@ proofs about these definitions, those are contained in other files in `Batteries
 
 namespace Array
 
-/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
-def reduceOption (l : Array (Option α)) : Array α :=
-  l.filterMap id
-
 /--
 Check whether `xs` and `ys` are equal as sets, i.e. they contain the same
 elements when disregarding order and duplicates. `O(n*m)`! If your element type
@@ -122,11 +119,7 @@ protected def maxI [ord : Ord α] [Inhabited α]
     (xs : Array α) (start := 0) (stop := xs.size) : α :=
   xs.minI (ord := ord.opposite) start stop
 
-/--
-`O(|join L|)`. `join L` concatenates all the arrays in `L` into one array.
-* `join #[#[a], #[], #[b, c], #[d, e, f]] = #[a, b, c, d, e, f]`
--/
-@[inline] def join (l : Array (Array α)) : Array α := l.foldl (· ++ ·) #[]
+@[deprecated (since := "2024-10-15")] alias join := flatten
 
 /-!
 ### Safe Nat Indexed Array functions

Batteries/Data/Array/Lemmas.lean

@@ -14,19 +14,8 @@ namespace Array
 theorem forIn_eq_forIn_toList [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn as b f = forIn as.toList b f := by
-  let rec loop : ∀ {i h b j}, j + i = as.size →
-      Array.forIn.loop as f i h b = forIn (as.toList.drop j) b f
-    | 0, _, _, _, rfl => by rw [List.drop_length]; rfl
-    | i+1, _, _, j, ij => by
-      simp only [forIn.loop, Nat.add]
-      have j_eq : j = size as - 1 - i := by simp [← ij, ← Nat.add_assoc]
-      have : as.size - 1 - i < as.size := j_eq ▸ ij ▸ Nat.lt_succ_of_le (Nat.le_add_right ..)
-      have : as[size as - 1 - i] :: as.toList.drop (j + 1) = as.toList.drop j := by
-        rw [j_eq]; exact List.getElem_cons_drop _ _ this
-      simp only [← this, List.forIn_cons]; congr; funext x; congr; funext b
-      rw [loop (i := i)]; rw [← ij, Nat.succ_add]; rfl
-  conv => lhs; simp only [forIn, Array.forIn]
-  rw [loop (Nat.zero_add _)]; rfl
+  cases as
+  simp
 
 @[deprecated (since := "2024-09-09")] alias forIn_eq_forIn_data := forIn_eq_forIn_toList
 @[deprecated (since := "2024-08-13")] alias forIn_eq_data_forIn := forIn_eq_forIn_data
@@ -99,28 +88,11 @@ theorem size_filter_le (p : α → Bool) (l : Array α) :
   simp only [← length_toList, toList_filter]
   apply List.length_filter_le
 
-/-! ### join -/
-
-@[simp] theorem toList_join {l : Array (Array α)} : l.join.toList = (l.toList.map toList).join := by
-  dsimp [join]
-  simp only [foldl_eq_foldl_toList]
-  generalize l.toList = l
-  have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
-  exact this #[]
-  induction l with
-  | nil => simp
-  | cons h => induction h.toList <;> simp [*]
-@[deprecated (since := "2024-09-09")] alias data_join := toList_join
-@[deprecated (since := "2024-08-13")] alias join_data := data_join
-
-theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l := by
-  simp only [mem_def, toList_join, List.mem_join, List.mem_map]
-  intro l
-  constructor
-  · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
-    exact ⟨s, m, h⟩
-  · rintro ⟨s, h₁, h₂⟩
-    refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
+/-! ### flatten -/
+
+@[deprecated (since := "2024-09-09")] alias data_join := toList_flatten
+@[deprecated (since := "2024-08-13")] alias join_data := toList_flatten
+@[deprecated (since := "2024-10-15")] alias mem_join := mem_flatten
 
 /-! ### indexOf? -/
 
@@ -154,27 +126,10 @@ where
     (a.eraseIdx i).size = if i < a.size then a.size-1 else a.size := by
   simp only [eraseIdx]; split; simp; rfl
 
-/-! ### shrink -/
-
-theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size - n := by
-  induction n generalizing a with simp only [shrink.loop, Nat.sub_zero]
-  | succ n ih => simp only [ih, size_pop]; omega
-
-@[simp] theorem size_shrink (a : Array α) (n) : (a.shrink n).size = min a.size n := by
-  simp [shrink, size_shrink_loop]
-  omega
-
 /-! ### set -/
 
 theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
 
-/-! ### swapAt -/
-
-theorem size_swapAt (a : Array α) (x i) : (a.swapAt i x).snd.size = a.size := by simp
-
-@[simp] theorem size_swapAt! (a : Array α) (x) (h : i < a.size) :
-    (a.swapAt! i x).snd.size = a.size := by simp [h]
-
 /-! ### map -/
 
 theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
@@ -266,14 +221,14 @@ theorem getElem_insertAt_lt (as : Array α) (i : Fin (as.size+1)) (v : α)
     (k) (hlt : k < i.val) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} :
     (as.insertAt i v)[k] = as[k] := by
   simp only [insertAt]
-  rw [get_insertAt_loop_lt, get_push, dif_pos hk']
+  rw [get_insertAt_loop_lt, getElem_push, dif_pos hk']
   exact hlt
 
 theorem getElem_insertAt_gt (as : Array α) (i : Fin (as.size+1)) (v : α)
     (k) (hgt : k > i.val) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} :
     (as.insertAt i v)[k] = as[k - 1] := by
   simp only [insertAt]
-  rw [get_insertAt_loop_gt_le, get_push, dif_pos hk']
+  rw [get_insertAt_loop_gt_le, getElem_push, dif_pos hk']
   exact hgt
   rw [size_insertAt] at hk
   exact Nat.le_of_lt_succ hk
@@ -282,6 +237,6 @@ theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α)
     (k) (heq : i.val = k) {hk : k < (as.insertAt i v).size} :
     (as.insertAt i v)[k] = v := by
   simp only [insertAt]
-  rw [get_insertAt_loop_eq, Fin.getElem_fin, get_push_eq]
+  rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq]
   exact heq
   exact Nat.le_of_lt_succ i.is_lt

Batteries/Data/Array/Match.lean

@@ -52,7 +52,7 @@ termination_by k => k.val
 def PrefixTable.extend [BEq α] (t : PrefixTable α) (x : α) : PrefixTable α where
   toArray := t.toArray.push (x, t.step x ⟨t.size, Nat.lt_succ_self _⟩)
   valid _ := by
-    rw [Array.get_push]
+    rw [Array.getElem_push]
     split
     · exact t.valid ..
     · next h => exact Nat.le_trans (Nat.lt_succ.1 <| Fin.isLt ..) (Nat.not_lt.1 h)

Batteries/Data/Array/Monadic.lean

@@ -44,7 +44,7 @@ theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m
   · case s =>
     intro ⟨i, hi⟩ arr ⟨ih₁, eq, ih₂⟩
     refine (hs _ ih₁).map fun ⟨h₁, h₂⟩ => ⟨h₂, by simp [eq], fun j hj => ?_⟩
-    simp [get_push] at hj ⊢; split; {apply ih₂}
+    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 β)
@@ -125,27 +125,36 @@ 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_mapIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Fin as.size → α → m β)
+theorem SatisfiesM_mapFinIdxM [Monad m] [LawfulMonad m] (as : Array α) (f : Fin 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])) :
     SatisfiesM
       (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
-      (Array.mapIdxM as f) := by
+      (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) :
     SatisfiesM
       (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
-      (Array.mapIdxM.map as f i j h bs) := by
-    induction i generalizing j bs with simp [mapIdxM.map]
+      (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
-      simp at hi'; simp [get_push]; split
+      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 [mapIdxM]; exact go rfl nofun h0
+  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])) :
+    SatisfiesM
+      (fun arr => motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i])
+      (Array.mapIdxM as f) :=
+  SatisfiesM_mapFinIdxM as (fun i => f i) 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

Batteries/Data/Array/Pairwise.lean

@@ -21,7 +21,7 @@ def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwi
 
 theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Fin as.size), i < j → R (as.get i) (as.get j) := by
-  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_toList_get]
+  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

Batteries/Data/AssocList.lean

@@ -244,8 +244,8 @@ instance : ForIn m (AssocList α β) (α × β) where
 
 @[simp] theorem forIn_eq [Monad m] (l : AssocList α β) (init : δ)
     (f : (α × β) → δ → m (ForInStep δ)) : forIn l init f = forIn l.toList init f := by
-  simp [forIn, List.forIn]
-  induction l generalizing init <;> simp [AssocList.forIn, List.forIn.loop]
+  simp only [forIn]
+  induction l generalizing init <;> simp [AssocList.forIn]
   congr; funext a; split <;> simp [*]
 
 /-- Split the list into head and tail, if possible. -/

Batteries/Data/ByteArray.lean

@@ -36,11 +36,11 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
   Array.size_push ..
 
 @[simp] theorem get_push_eq (a : ByteArray) (x : UInt8) : (a.push x)[a.size] = x :=
-  Array.get_push_eq ..
+  Array.getElem_push_eq ..
 
 theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
     (a.push x)[i]'(size_push .. ▸ Nat.lt_succ_of_lt h) = a[i] :=
-  Array.get_push_lt ..
+  Array.getElem_push_lt ..
 
 /-! ### set -/
 

Batteries/Data/HashMap/Basic.lean

@@ -37,7 +37,7 @@ def update (data : Buckets α β) (i : USize)
 The number of elements in the bucket array.
 Note: this is marked `noncomputable` because it is only intended for specification.
 -/
-noncomputable def size (data : Buckets α β) : Nat := .sum (data.1.toList.map (·.toList.length))
+noncomputable def size (data : Buckets α β) : Nat := (data.1.toList.map (·.toList.length)).sum
 
 @[simp] theorem update_size (self : Buckets α β) (i d h) :
     (self.update i d h).1.size = self.1.size := Array.size_uset ..
@@ -56,7 +56,7 @@ structure WF [BEq α] [Hashable α] (buckets : Buckets α β) : Prop where
     bucket.toList.Pairwise fun a b => ¬(a.1 == b.1)
   /-- Every element in a bucket should hash to its location. -/
   hash_self (i : Nat) (h : i < buckets.1.size) :
-    buckets.1[i].All fun k _ => ((hash k).toUSize % buckets.1.size).toNat = i
+    buckets.1[i].All fun k _ => ((hash k).toUSize % USize.ofNat buckets.1.size).toNat = i
 
 end Buckets
 end Imp
@@ -93,7 +93,7 @@ def empty (capacity := 0) : Imp α β :=
 
 /-- Calculates the bucket index from a hash value `u`. -/
 def mkIdx {n : Nat} (h : 0 < n) (u : USize) : {u : USize // u.toNat < n} :=
-  ⟨u % n, USize.modn_lt _ h⟩
+  ⟨u % USize.ofNat n, USize.toNat_mod_lt _ h⟩
 
 /--
 Inserts a key-value pair into the bucket array. This function assumes that the data is not