Trigger CI for leanprover/lean4#5991

.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,6 +31,7 @@ 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.UInt
 import Batteries.Data.UnionFind
@@ -93,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/Lemmas.lean

@@ -22,61 +22,13 @@ theorem forIn_eq_forIn_toList [Monad m]
 
 /-! ### zipWith / zip -/
 
-theorem toList_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
-    (as.zipWith bs f).toList = as.toList.zipWith f bs.toList := by
-  let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
-      (zipWithAux f as bs i cs).toList =
-        cs.toList ++ (as.toList.drop i).zipWith f (bs.toList.drop i) := by
-    intro i cs hia hib
-    unfold zipWithAux
-    by_cases h : i = as.size ∨ i = bs.size
-    case pos =>
-      have : ¬(i < as.size) ∨ ¬(i < bs.size) := by
-        cases h <;> simp_all only [Nat.not_lt, Nat.le_refl, true_or, or_true]
-      -- Cleaned up aesop output below
-      simp_all only [Nat.not_lt]
-      cases h <;> [(cases this); (cases this)]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_left, List.append_nil]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_left, List.append_nil]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_right, List.append_nil]
-        split <;> simp_all only [Nat.not_lt]
-      · simp_all only [Nat.le_refl, Nat.lt_irrefl, dite_false, List.drop_length,
-                      List.zipWith_nil_right, List.append_nil]
-        split <;> simp_all only [Nat.not_lt]
-    case neg =>
-      rw [not_or] at h
-      have has : i < as.size := Nat.lt_of_le_of_ne hia h.1
-      have hbs : i < bs.size := Nat.lt_of_le_of_ne hib h.2
-      simp only [has, hbs, dite_true]
-      rw [loop (i+1) _ has hbs, Array.push_toList]
-      have h₁ : [f as[i] bs[i]] = List.zipWith f [as[i]] [bs[i]] := rfl
-      let i_as : Fin as.toList.length := ⟨i, has⟩
-      let i_bs : Fin bs.toList.length := ⟨i, hbs⟩
-      rw [h₁, List.append_assoc]
-      congr
-      rw [← List.zipWith_append (h := by simp), getElem_eq_getElem_toList,
-        getElem_eq_getElem_toList]
-      show List.zipWith f (as.toList[i_as] :: List.drop (i_as + 1) as.toList)
-        ((List.get bs.toList i_bs) :: List.drop (i_bs + 1) bs.toList) =
-        List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)
-      simp only [length_toList, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
-  simp [zipWith, loop 0 #[] (by simp) (by simp)]
 @[deprecated (since := "2024-09-09")] alias data_zipWith := toList_zipWith
 @[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
 @[simp] theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by
   rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
 
-theorem toList_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).toList = as.toList.zip bs.toList :=
-  toList_zipWith Prod.mk as bs
-@[deprecated (since := "2024-09-09")] alias data_zip := toList_zip
-@[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip
-
 @[simp] theorem size_zip (as : Array α) (bs : Array β) :
     (as.zip bs).size = min as.size bs.size :=
   as.size_zipWith bs Prod.mk