chore: merge main

.github/workflows/build.yml

@@ -54,4 +54,4 @@ jobs:
       - name: Don't 'import Lean', use precise imports
         if: always()
         run: |
-          ! (find . -name "*.lean" ! -path "./test/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
+          ! (find . -name "*.lean" ! -path "./BatteriesTest/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')

.github/workflows/labels-from-status.yml

@@ -0,0 +1,62 @@
+# This workflow assigns `awaiting-review` or `WIP` labels to new PRs, and it removes
+# `awaiting-review`, `awaiting-author`, or `WIP` label from closed PRs.
+# It does not modify labels for open PRs that already have one of the `awaiting-review`,
+# `awaiting-author`, or `WIP` labels.
+
+name: Label PR from status change
+
+permissions:
+  contents: read
+  pull-requests: write
+
+on:
+  pull_request:
+    types:
+      - closed
+      - opened
+      - reopened
+      - converted_to_draft
+      - ready_for_review
+    branches:
+      - main
+
+jobs:
+  auto-label:
+    if: github.repository_owner == 'leanprover-community'
+    runs-on: ubuntu-latest
+    steps:
+
+    - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+
+    - name: Unlabel closed PR
+      if: github.event.pull_request.state == 'closed'
+      uses: actions-ecosystem/action-remove-labels@v1
+      with:
+        labels: |
+          WIP
+          awaiting-author
+          awaiting-review
+
+    - name: Label unlabeled draft PR as WIP
+      if: |
+        github.event.pull_request.state == 'open' &&
+        github.event.pull_request.draft &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-author') &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-review') &&
+        ! contains(github.event.pull_request.labels.*.name, 'WIP')
+      uses: actions-ecosystem/action-add-labels@v1
+      with:
+        labels: WIP
+
+    - name: Label unlabeled other PR as awaiting-review
+      if: |
+        github.event.pull_request.state == 'open' &&
+        ! github.event.pull_request.draft &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-author') &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-review') &&
+        ! contains(github.event.pull_request.labels.*.name, 'WIP')
+      uses: actions-ecosystem/action-add-labels@v1
+      with:
+        labels: awaiting-review

Batteries.lean

@@ -31,8 +31,8 @@ import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 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
@@ -71,7 +71,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
@@ -95,9 +94,6 @@ import Batteries.Tactic.SqueezeScope
 import Batteries.Tactic.Trans
 import Batteries.Tactic.Unreachable
 import Batteries.Tactic.Where
-import Batteries.Test.Internal.DummyLabelAttr
-import Batteries.Test.Internal.DummyLibraryNote
-import Batteries.Test.Internal.DummyLibraryNote2
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote

Batteries/CodeAction/Misc.lean

@@ -3,11 +3,9 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Elab.BuiltinTerm
-import Lean.Elab.BuiltinNotation
+import Lean.Elab.Tactic.Induction
 import Batteries.Lean.Position
 import Batteries.CodeAction.Attr
-import Lean.Meta.Tactic.TryThis
 import Lean.Server.CodeActions.Provider
 
 /-!
@@ -236,28 +234,39 @@ def removeAfterDoneAction : TacticCodeAction := fun _ _ _ stk node => do
   pure #[{ eager }]
 
 /--
-Similar to `getElabInfo`, but returns the names of binders instead of just the numbers;
+Similar to `getElimExprInfo`, but returns the names of binders instead of just the numbers;
 intended for code actions which need to name the binders.
 -/
-def getElimNames (inductName declName : Name) : MetaM (Array (Name × Array Name)) := do
-  let inductVal ← getConstInfoInduct inductName
-  let decl ← getConstInfo declName
-  forallTelescopeReducing decl.type fun xs type => do
+def getElimExprNames (elimType : Expr) : MetaM (Array (Name × Array Name)) := do
+  -- let inductVal ← getConstInfoInduct inductName
+  -- let decl ← getConstInfo declName
+  forallTelescopeReducing elimType fun xs type => do
     let motive  := type.getAppFn
     let targets := type.getAppArgs
+    let motiveType ← inferType motive
     let mut altsInfo := #[]
-    for i in [inductVal.numParams:xs.size] do
-      let x := xs[i]!
+    for _h : i in [:xs.size] do
+      let x := xs[i]
       if x != motive && !targets.contains x then
         let xDecl ← x.fvarId!.getDecl
-        let args ← forallTelescopeReducing xDecl.type fun args _ => do
-          let lctx ← getLCtx
-          pure <| args.filterMap fun y =>
-            let yDecl := (lctx.find? y.fvarId!).get!
-            if yDecl.binderInfo.isExplicit then some yDecl.userName else none
-        altsInfo := altsInfo.push (xDecl.userName, args)
+        if xDecl.binderInfo.isExplicit then
+          let args ← forallTelescopeReducing xDecl.type fun args _ => do
+            let lctx ← getLCtx
+            pure <| args.filterMap fun y =>
+              let yDecl := (lctx.find? y.fvarId!).get!
+              if yDecl.binderInfo.isExplicit then some yDecl.userName else none
+          altsInfo := altsInfo.push (xDecl.userName, args)
     pure altsInfo
 
+/-- Finds the `TermInfo` for an elaborated term `stx`. -/
+def findTermInfo? (node : InfoTree) (stx : Term) : Option TermInfo :=
+  match node.findInfo? fun
+    | .ofTermInfo i => i.stx.getKind == stx.raw.getKind && i.stx.getRange? == stx.raw.getRange?
+    | _ => false
+  with
+  | some (.ofTermInfo info) => pure info
+  | _ => none
+
 /--
 Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the
 following:
@@ -278,18 +287,39 @@ It also works for `cases`.
 @[tactic_code_action Parser.Tactic.cases Parser.Tactic.induction]
 def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
   let .node (.ofTacticInfo info) _ := node | return #[]
-  let (discr, induction, alts) ← match info.stx with
-    | `(tactic| cases $[$_ :]? $e $[$alts:inductionAlts]?) => pure (e, false, alts)
-    | `(tactic| induction $e $[generalizing $_*]? $[$alts:inductionAlts]?) => pure (e, true, alts)
+  let (targets, induction, using_, alts) ← match info.stx with
+    | `(tactic| cases $[$[$_ :]? $targets],* $[using $u]? $(alts)?) =>
+      pure (targets, false, u, alts)
+    | `(tactic| induction $[$targets],* $[using $u]? $[generalizing $_*]? $(alts)?) =>
+      pure (targets, true, u, alts)
     | _ => return #[]
-  if let some alts := alts then
-    -- this detects the incomplete syntax `cases e with`
-    unless alts.raw[2][0][0][0][0].isMissing do return #[]
-  let some (.ofTermInfo discrInfo) := node.findInfo? fun i =>
-    i.stx.getKind == discr.raw.getKind && i.stx.getRange? == discr.raw.getRange?
-    | return #[]
-  let .const name _ := (← discrInfo.runMetaM ctx (do whnf (← inferType discrInfo.expr))).getAppFn
+  let some discrInfos := targets.mapM (findTermInfo? node) | return #[]
+  let some discr₀ := discrInfos[0]? | return #[]
+  let mut some ctors ← discr₀.runMetaM ctx do
+      let targets := discrInfos.map (·.expr)
+      match using_ with
+      | none =>
+        if Tactic.tactic.customEliminators.get (← getOptions) then
+          if let some elimName ← getCustomEliminator? targets induction then
+            return some (← getElimExprNames (← getConstInfo elimName).type)
+        matchConstInduct (← whnf (← inferType discr₀.expr)).getAppFn
+            (fun _ => failure) fun val _ => do
+          let elimName := if induction then mkRecName val.name else mkCasesOnName val.name
+          return some (← getElimExprNames (← getConstInfo elimName).type)
+      | some u =>
+        let some info := findTermInfo? node u | return none
+        return some (← getElimExprNames (← inferType info.expr))
     | return #[]
+  let mut fallback := none
+  if let some alts := alts then
+    if let `(Parser.Tactic.inductionAlts| with $(_)? $alts*) := alts then
+      for alt in alts do
+        match alt with
+        | `(Parser.Tactic.inductionAlt| | _ $_* => $fb) => fallback := fb.raw.getRange?
+        | `(Parser.Tactic.inductionAlt| | $id:ident $_* => $_) =>
+          ctors := ctors.filter (fun x => x.1 != id.getId)
+        | _ => pure ()
+  if ctors.isEmpty then return #[]
   let tacName := info.stx.getKind.updatePrefix .anonymous
   let eager := {
     title := s!"Generate an explicit pattern match for '{tacName}'."
@@ -301,15 +331,21 @@ def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
     lazy? := some do
       let tacPos := info.stx.getPos?.get!
       let endPos := doc.meta.text.utf8PosToLspPos info.stx.getTailPos?.get!
-      let startPos := if alts.isSome then
-        let stx' := info.stx.setArg (if induction then 4 else 3) mkNullNode
-        doc.meta.text.utf8PosToLspPos stx'.getTailPos?.get!
-      else endPos
-      let elimName := if induction then mkRecName name else mkCasesOnName name
-      let ctors ← discrInfo.runMetaM ctx (getElimNames name elimName)
-      let newText := if ctors.isEmpty then "" else Id.run do
-        let mut str := " with"
-        let indent := "\n".pushn ' ' (findIndentAndIsStart doc.meta.text.source tacPos).1
+      let indent := "\n".pushn ' ' (findIndentAndIsStart doc.meta.text.source tacPos).1
+      let (startPos, str') := if alts.isSome then
+        let stx' := if fallback.isSome then
+          info.stx.modifyArg (if induction then 4 else 3)
+            (·.modifyArg 0 (·.modifyArg 2 (·.modifyArgs (·.filter fun s =>
+              !(s matches `(Parser.Tactic.inductionAlt| | _ $_* => $_))))))
+        else info.stx
+        (doc.meta.text.utf8PosToLspPos stx'.getTailPos?.get!, "")
+      else (endPos, " with")
+      let fallback := if let some ⟨startPos, endPos⟩ := fallback then
+        doc.meta.text.source.extract startPos endPos
+      else
+        "sorry"
+      let newText := Id.run do
+        let mut str := str'
         for (name, args) in ctors do
           let mut ctor := toString name
           if let some _ := (Parser.getTokenTable snap.env).find? ctor then
@@ -324,7 +360,7 @@ def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
           else args
           for arg in args do
             str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
-          str := str ++ s!" => sorry"
+          str := str ++ s!" => " ++ fallback
         str
       pure { eager with
         edit? := some <|.ofTextEdit doc.versionedIdentifier {

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