merge main

.github/workflows/build.yml

@@ -20,7 +20,7 @@ jobs:
         name: build, test, and lint batteries
         uses: leanprover/lean-action@v1
         with:
-          build-args: '-Kwerror'
+          build-args: '--wfail'
 
       - name: Check that all files are imported
         run: lake env lean scripts/check_imports.lean

.github/workflows/test_mathlib.yml

@@ -0,0 +1,97 @@
+# Test Mathlib against a Batteries PR
+
+name: Test Mathlib
+
+on:
+  workflow_run:
+    workflows: [ci]
+    types: [completed]
+
+jobs:
+  on-success:
+    runs-on: ubuntu-latest
+    if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover-community/batteries'
+    steps:
+      - name: Retrieve information about the original workflow
+        uses: potiuk/get-workflow-origin@v1_1
+        id: workflow-info
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          sourceRunId: ${{ github.event.workflow_run.id }}
+
+      - name: Checkout mathlib4 repository
+        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        uses: actions/checkout@v4
+        with:
+          repository: leanprover-community/mathlib4
+          token: ${{ secrets.MATHLIB4_BOT }}
+          ref: master
+          fetch-depth: 0
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+      - name: Retrieve PR information
+        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        id: pr-info
+        uses: actions/github-script@v6
+        env:
+          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
+        with:
+          script: |
+            const prNumber = process.env.PR_NUMBER;
+            const { data: pr } = await github.rest.pulls.get({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              pull_number: prNumber
+            });
+            core.exportVariable('HEAD_REPO', pr.head.repo.full_name);
+            core.exportVariable('HEAD_BRANCH', pr.head.ref);
+
+      - name: Check if tag exists
+        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        id: check_mathlib_tag
+        env:
+          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          HEAD_REPO: ${{ env.HEAD_REPO }}
+          HEAD_BRANCH: ${{ env.HEAD_BRANCH }}
+        run: |
+          git config user.name "leanprover-community-mathlib4-bot"
+          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
+
+          echo "PR info: $HEAD_REPO $HEAD_BRANCH"
+
+          BASE=master
+          echo "Using base tag: $BASE"
+
+          EXISTS="$(git ls-remote --heads origin batteries-pr-testing-$PR_NUMBER | wc -l)"
+          echo "Branch exists: $EXISTS"
+          if [ "$EXISTS" = "0" ]; then
+            echo "Branch does not exist, creating it."
+            git switch -c batteries-pr-testing-$PR_NUMBER "$BASE"
+
+            # Use the fork and branch name to modify the lakefile.lean
+            sed -i "s,require \"leanprover-community\" / \"batteries\" @ git \".\+\",require \"leanprover-community\" / \"batteries\" from git \"https://github.com/$HEAD_REPO\" @ \"$HEAD_BRANCH\",g" lakefile.lean
+
+            lake update batteries
+            git add lakefile.lean lake-manifest.json
+            git commit -m "Update Batteries branch for testing https://github.com/leanprover-community/batteries/pull/$PR_NUMBER"
+          else
+            echo "Branch already exists, merging $BASE and bumping Batteries."
+            git switch batteries-pr-testing-$PR_NUMBER
+            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
+            lake update batteries
+            git add lake-manifest.json
+            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover-community/batteries/pull/$PR_NUMBER"
+          fi
+
+      - name: Push changes
+        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        env:
+          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
+        run: |
+          git push origin batteries-pr-testing-$PR_NUMBER

Batteries/CodeAction/Attr.lean

@@ -14,7 +14,7 @@ import Lean.Server.CodeActions.Basic
 * Attribute `@[tactic_code_action]` collects code actions which will be called
   on each occurrence of a tactic.
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
 open Lean Elab Server Lsp RequestM Snapshots
 

Batteries/CodeAction/Basic.lean

@@ -19,7 +19,7 @@ on each occurrence of a hole (`_`, `?_` or `sorry`).
 attempt to use this code action provider when browsing the `Batteries.CodeAction.Hole.Attr` file
 itself.)
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
 open Lean Elab Server RequestM CodeAction
 

Batteries/CodeAction/Deprecated.lean

@@ -14,7 +14,9 @@ This is an opt-in mechanism for making machine-applicable `@[deprecated]` defini
 whenever the deprecation lint also fires, allowing the user to replace the usage of the deprecated
 constant.
 -/
-namespace Std
+
+namespace Batteries
+
 open Lean Elab Server Lsp RequestM CodeAction
 
 /-- An environment extension for identifying `@[deprecated]` definitions which can be auto-fixed -/

Batteries/CodeAction/Misc.lean

@@ -15,7 +15,7 @@ import Lean.Server.CodeActions.Provider
 
 This declares some basic tactic code actions, using the `@[tactic_code_action]` API.
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
 open Lean Meta Elab Server RequestM CodeAction
 

Batteries/Data/Array.lean

@@ -4,4 +4,5 @@ import Batteries.Data.Array.Lemmas
 import Batteries.Data.Array.Match
 import Batteries.Data.Array.Merge
 import Batteries.Data.Array.Monadic
+import Batteries.Data.Array.OfFn
 import Batteries.Data.Array.Pairwise

Batteries/Data/Array/Lemmas.lean

@@ -122,10 +122,64 @@ theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L 
   · rintro ⟨s, h₁, h₂⟩
     refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
 
+/-! ### indexOf? -/
+
+theorem indexOf?_data [BEq α] {a : α} {l : Array α} :
+    l.data.indexOf? a = (l.indexOf? a).map Fin.val := by
+  simpa using aux l 0
+where
+  aux (l : Array α) (i : Nat) :
+       ((l.data.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by
+    rw [indexOfAux]
+    if h : i < l.size then
+      rw [List.drop_eq_getElem_cons h, ←getElem_eq_data_getElem, List.indexOf?_cons]
+      if h' : l[i] == a then
+        simp [h, h']
+      else
+        simp [h, h', ←aux l (i+1), Function.comp_def, ←Nat.add_assoc, Nat.add_right_comm]
+    else
+      have h' : l.size ≤ i := Nat.le_of_not_lt h
+      simp [h, List.drop_of_length_le h', List.indexOf?]
+  termination_by l.size - i
+
 /-! ### erase -/
 
-@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
-    (l.erase a).toList = l.toList.erase a
+theorem eraseIdx_data_swap {l : Array α} (i : Nat) (lt : i + 1 < size l) :
+    (l.swap ⟨i+1, lt⟩ ⟨i, Nat.lt_of_succ_lt lt⟩).data.eraseIdx (i+1) = l.data.eraseIdx i := by
+  let ⟨xs⟩ := l
+  induction i generalizing xs <;> let x₀::x₁::xs := xs
+  case zero => simp [swap, get]
+  case succ i ih _ =>
+    have lt' := Nat.lt_of_succ_lt_succ lt
+    have : (swap ⟨x₀::x₁::xs⟩ ⟨i.succ + 1, lt⟩ ⟨i.succ, Nat.lt_of_succ_lt lt⟩).data
+        = x₀::(swap ⟨x₁::xs⟩ ⟨i + 1, lt'⟩ ⟨i, Nat.lt_of_succ_lt lt'⟩).data := by
+      simp [swap_def, getElem_eq_data_getElem]
+    simp [this, ih]
+
+@[simp] theorem data_feraseIdx {l : Array α} (i : Fin l.size) :
+    (l.feraseIdx i).data = l.data.eraseIdx i := by
+  induction l, i using feraseIdx.induct with
+  | @case1 a i lt a' i' ih =>
+    rw [feraseIdx]
+    simp [lt, ih, a', eraseIdx_data_swap i lt]
+  | case2 a i lt =>
+    have : i + 1 ≥ a.size := Nat.ge_of_not_lt lt
+    have last : i + 1 = a.size := Nat.le_antisymm i.is_lt this
+    simp [feraseIdx, lt, List.dropLast_eq_eraseIdx last]
+
+@[simp] theorem data_erase [BEq α] (l : Array α) (a : α) : (l.erase a).data = l.data.erase a := by
+  match h : indexOf? l a with
+  | none =>
+    simp only [erase, h]
+    apply Eq.symm
+    rw [List.erase_eq_self_iff_forall_bne, ←List.indexOf?_eq_none_iff, indexOf?_data,
+        h, Option.map_none']
+  | some i =>
+    simp only [erase, h]
+    rw [data_feraseIdx, ←List.eraseIdx_indexOf_eq_erase]
+    congr
+    rw [List.indexOf_eq_indexOf?, indexOf?_data]
+    simp [h]
 
 /-! ### shrink -/
 

Batteries/Data/Array/OfFn.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Batteries.Data.List.OfFn
+
+open List
+
+namespace Array
+
+/-! ### ofFn -/
+
+@[simp]
+theorem data_ofFn (f : Fin n → α) : (ofFn f).data = List.ofFn f := by
+  ext1
+  simp only [getElem?_eq, data_length, size_ofFn, length_ofFn, getElem_ofFn]
+  split
+  · rw [← getElem_eq_data_getElem]
+    simp
+  · rfl
+
+end Array

Batteries/Data/Fin/Lemmas.lean

@@ -44,14 +44,14 @@ theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
 theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
   rw [list_succ]
   induction n with
-  | zero => simp
+  | zero => simp [last]
   | succ n ih =>
     rw [list_succ, List.map_cons castSucc, ih]
     simp [Function.comp_def, succ_castSucc]
 
 theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
   induction n with
-  | zero => simp
+  | zero => simp [last]
   | succ n ih =>
     conv => lhs; rw [list_succ_last]
     conv => rhs; rw [list_succ]

Batteries/Data/HashMap/WF.lean

@@ -96,12 +96,14 @@ where
         .sum (source.toList.map (·.toList.length)) + target.size := by
     unfold expand.go; split
     · next H =>
-      refine (go (i+1) _ _ fun j hj => ?a).trans ?b <;> simp
+      refine (go (i+1) _ _ fun j hj => ?a).trans ?b
       · case a =>
+        simp only [Array.data_length, Array.data_set]
         simp [List.getD_eq_getElem?_getD, List.getElem?_set, Option.map_eq_map]; split
         · cases source.toList[j]? <;> rfl
         · next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H))
       · case b =>
+        simp only [Array.data_length, Array.data_set, Array.get_eq_getElem, AssocList.foldl_eq]
         refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set H; eq ▸ ?_
         rw [h₁]
         simp only [Buckets.size_eq, List.map_append, List.map_cons, AssocList.toList,

Batteries/Data/List.lean

@@ -3,5 +3,6 @@ import Batteries.Data.List.Count
 import Batteries.Data.List.EraseIdx
 import Batteries.Data.List.Init.Lemmas
 import Batteries.Data.List.Lemmas
+import Batteries.Data.List.OfFn
 import Batteries.Data.List.Pairwise
 import Batteries.Data.List.Perm

Batteries/Data/List/Basic.lean

@@ -602,28 +602,7 @@ def sigmaTR {σ : α → Type _} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
 ofFn f = [f 0, f 1, ... , f (n - 1)]
 ```
 -/
-def ofFn {n} (f : Fin n → α) : List α := go n 0 rfl where
-  /-- Auxiliary for `List.ofFn`. `ofFn.go f i j _ = [f j, ..., f (n - 1)]`. -/
-  -- This used to be defined via `Array.ofFn` but mathlib relies on reducing it,
-  -- so we use a structurally recursive definition here.
-  go : (i j : Nat) → (h : i + j = n) → List α
-  | 0, _, _ => []
-  | i+1, j, h => f ⟨j, by omega⟩ :: go i (j+1) (Nat.add_right_comm .. ▸ h :)
-
-/-- Tail-recursive version of `ofFn`. -/
-@[inline] def ofFnTR {n} (f : Fin n → α) : List α := go n (Nat.le_refl _) [] where
-  /-- Auxiliary for `List.ofFnTR`. `ofFnTR.go f i _ acc = f 0 :: ... :: f (i - 1) :: acc`. -/
-  go : (i : Nat) → (h : i ≤ n) → List α → List α
-  | 0, _, acc => acc
-  | i+1, h, acc => go i (Nat.le_of_lt h) (f ⟨i, h⟩ :: acc)
-
-@[csimp] theorem ofFn_eq_ofFnTR : @ofFn = @ofFnTR := by
-  funext α n f; simp [ofFnTR]
-  let rec go (i j h h') : ofFnTR.go f j h' (ofFn.go f i j h) = ofFn f := by
-    unfold ofFnTR.go; split
-    · subst h; rfl
-    · next l j h' => exact go (i+1) j ((Nat.succ_add ..).trans h) (Nat.le_of_lt h')
-  exact (go 0 n (Nat.zero_add _) (Nat.le_refl _)).symm
+def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) []
 
 /-- `ofFnNthVal f i` returns `some (f i)` if `i < n` and `none` otherwise. -/
 def ofFnNthVal {n} (f : Fin n → α) (i : Nat) : Option α :=