Trigger CI for leanprover/lean4#4325

.github/workflows/build.yml

@@ -18,10 +18,9 @@ jobs:
 
       - id: lean-action
         name: build, test, and lint batteries
-        uses: leanprover/lean-action@v1-beta
+        uses: leanprover/lean-action@v1
         with:
           build-args: '-Kwerror'
-          lint-module: 'Batteries'
 
       - name: Check that all files are imported
         run: lake env lean scripts/check_imports.lean

Batteries.lean

@@ -1,4 +1,3 @@
-import Batteries.Classes.BEq
 import Batteries.Classes.Cast
 import Batteries.Classes.Order
 import Batteries.Classes.RatCast
@@ -15,10 +14,12 @@ import Batteries.Control.Lemmas
 import Batteries.Control.Nondet.Basic
 import Batteries.Data.Array
 import Batteries.Data.AssocList
+import Batteries.Data.BinaryHeap
 import Batteries.Data.BinomialHeap
 import Batteries.Data.BitVec
 import Batteries.Data.Bool
 import Batteries.Data.ByteArray
+import Batteries.Data.ByteSubarray
 import Batteries.Data.Char
 import Batteries.Data.DList
 import Batteries.Data.Fin
@@ -37,6 +38,7 @@ import Batteries.Data.String
 import Batteries.Data.Sum
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
+import Batteries.Data.Vector
 import Batteries.Lean.AttributeExtra
 import Batteries.Lean.Delaborator
 import Batteries.Lean.Except
@@ -57,18 +59,15 @@ import Batteries.Lean.Meta.SavedState
 import Batteries.Lean.Meta.Simp
 import Batteries.Lean.Meta.UnusedNames
 import Batteries.Lean.MonadBacktrack
-import Batteries.Lean.Name
 import Batteries.Lean.NameMap
 import Batteries.Lean.NameMapAttribute
 import Batteries.Lean.PersistentHashMap
 import Batteries.Lean.PersistentHashSet
 import Batteries.Lean.Position
-import Batteries.Lean.SMap
 import Batteries.Lean.Syntax
 import Batteries.Lean.System.IO
 import Batteries.Lean.TagAttribute
 import Batteries.Lean.Util.EnvSearch
-import Batteries.Lean.Util.Path
 import Batteries.Linter
 import Batteries.Linter.UnnecessarySeqFocus
 import Batteries.Linter.UnreachableTactic
@@ -82,6 +81,7 @@ import Batteries.Tactic.Congr
 import Batteries.Tactic.Exact
 import Batteries.Tactic.Init
 import Batteries.Tactic.Instances
+import Batteries.Tactic.Lemma
 import Batteries.Tactic.Lint
 import Batteries.Tactic.Lint.Basic
 import Batteries.Tactic.Lint.Frontend
@@ -100,7 +100,6 @@ import Batteries.Tactic.Unreachable
 import Batteries.Tactic.Where
 import Batteries.Test.Internal.DummyLabelAttr
 import Batteries.Util.Cache
-import Batteries.Util.CheckTactic
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote
 import Batteries.Util.Pickle

Batteries/Classes/Order.lean

@@ -102,7 +102,7 @@ theorem cmp_congr_left (xy : cmp x y = .eq) : cmp x z = cmp y z :=
 theorem cmp_congr_left' (xy : cmp x y = .eq) : cmp x = cmp y :=
   funext fun _ => cmp_congr_left xy
 
-theorem cmp_congr_right [TransCmp cmp] (yz : cmp y z = .eq) : cmp x y = cmp x z := by
+theorem cmp_congr_right (yz : cmp y z = .eq) : cmp x y = cmp x z := by
   rw [← Ordering.swap_inj, symm, symm, cmp_congr_left yz]
 
 end TransCmp
@@ -278,11 +278,8 @@ instance [Ord β] [OrientedOrd β] (f : α → β) : OrientedCmp (compareOn f) w
 instance [Ord β] [TransOrd β] (f : α → β) : TransCmp (compareOn f) where
   le_trans := TransCmp.le_trans (α := β)
 
--- FIXME: remove after lean4#3882 is merged
 theorem _root_.lexOrd_def [Ord α] [Ord β] :
-    (lexOrd : Ord (α × β)).compare = compareLex (compareOn (·.1)) (compareOn (·.2)) := by
-  funext a b
-  simp [lexOrd, compareLex, compareOn]
+    (lexOrd : Ord (α × β)).compare = compareLex (compareOn (·.1)) (compareOn (·.2)) := rfl
 
 section «non-canonical instances»
 -- Note: the following instances seem to cause lean to fail, see:

Batteries/CodeAction/Attr.lean

@@ -3,7 +3,7 @@ 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.Server.CodeActions
+import Lean.Server.CodeActions.Basic
 
 /-!
 # Initial setup for code action attributes

Batteries/CodeAction/Deprecated.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Server.CodeActions
 import Batteries.CodeAction.Basic
-import Batteries.Lean.Position
 
 /-!
 # Code action for @[deprecated] replacements
@@ -32,7 +31,7 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
   for m in snap.msgLog.toList do
     if m.data.isDeprecationWarning then
       if h : _ then
-        msgs := msgs.push (snap.cmdState.messages.toList[i])
+        msgs := msgs.push (snap.cmdState.messages.toList[i]'h)
     i := i + 1
   if msgs.isEmpty then return #[]
   let start := doc.meta.text.lspPosToUtf8Pos params.range.start

Batteries/CodeAction/Misc.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
-import Batteries.Lean.Name
 import Batteries.Lean.Position
 import Batteries.CodeAction.Attr
 import Lean.Meta.Tactic.TryThis

Batteries/Data/Array/Basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg
 -/
-import Batteries.Data.List.Init.Attach
 import Batteries.Data.Array.Init.Lemmas
 
 /-!
@@ -130,23 +129,6 @@ protected def maxI [ord : Ord α] [Inhabited α]
     (xs : Array α) (start := 0) (stop := xs.size) : α :=
   xs.minI (ord := ord.opposite) start stop
 
-/--
-Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
-`Array {x // P x}` is the same as the input `Array α`.
--/
-@[inline] private unsafe def attachWithImpl
-    (xs : Array α) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Array {x // P x} := unsafeCast xs
-
-/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array
-  with the same elements but in the type `{x // P x}`. -/
-@[implemented_by attachWithImpl] def attachWith
-    (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
-  ⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩
-
-/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
-  with the same elements but in the type `{x // x ∈ xs}`. -/
-@[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
-
 /--
 `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]`

Batteries/Data/Array/Lemmas.lean

@@ -11,7 +11,7 @@ import Batteries.Util.ProofWanted
 
 namespace Array
 
-theorem forIn_eq_data_forIn [Monad m]
+theorem forIn_eq_forIn_data [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn as b f = forIn as.data b f := by
   let rec loop : ∀ {i h b j}, j + i = as.size →
@@ -22,15 +22,16 @@ theorem forIn_eq_data_forIn [Monad m]
       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.data.drop (j + 1) = as.data.drop j := by
-        rw [j_eq]; exact List.get_cons_drop _ ⟨_, this⟩
+        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
+@[deprecated (since := "2024-08-13")] alias forIn_eq_data_forIn := forIn_eq_forIn_data
 
 /-! ### zipWith / zip -/
 
-theorem zipWith_eq_zipWith_data (f : α → β → γ) (as : Array α) (bs : Array β) :
+theorem data_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
     (as.zipWith bs f).data = as.data.zipWith f bs.data := by
   let rec loop : ∀ (i : Nat) cs, i ≤ as.size → i ≤ bs.size →
       (zipWithAux f as bs i cs).data = cs.data ++ (as.data.drop i).zipWith f (bs.data.drop i) := by
@@ -64,21 +65,22 @@ theorem zipWith_eq_zipWith_data (f : α → β → γ) (as : Array α) (bs : Arr
       let i_bs : Fin bs.data.length := ⟨i, hbs⟩
       rw [h₁, List.append_assoc]
       congr
-      rw [← List.zipWith_append (h := by simp), getElem_eq_data_get, getElem_eq_data_get]
-      show List.zipWith f ((List.get as.data i_as) :: List.drop (i_as + 1) as.data)
+      rw [← List.zipWith_append (h := by simp), getElem_eq_data_getElem, getElem_eq_data_getElem]
+      show List.zipWith f (as.data[i_as] :: List.drop (i_as + 1) as.data)
         ((List.get bs.data i_bs) :: List.drop (i_bs + 1) bs.data) =
         List.zipWith f (List.drop i as.data) (List.drop i bs.data)
-      simp only [List.get_cons_drop]
-    termination_by as.size - i
+      simp only [data_length, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
   simp [zipWith, loop 0 #[] (by simp) (by simp)]
+@[deprecated (since := "2024-08-13")] alias zipWith_eq_zipWith_data := data_zipWith
 
 theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by
-  rw [size_eq_length_data, zipWith_eq_zipWith_data, List.length_zipWith]
+  rw [size_eq_length_data, data_zipWith, List.length_zipWith]
 
-theorem zip_eq_zip_data (as : Array α) (bs : Array β) :
+theorem data_zip (as : Array α) (bs : Array β) :
     (as.zip bs).data = as.data.zip bs.data :=
-  zipWith_eq_zipWith_data Prod.mk as bs
+  data_zipWith Prod.mk as bs
+@[deprecated (since := "2024-08-13")] alias zip_eq_zip_data := data_zip
 
 theorem size_zip (as : Array α) (bs : Array β) :
     (as.zip bs).size = min as.size bs.size :=
@@ -93,7 +95,7 @@ theorem size_filter_le (p : α → Bool) (l : Array α) :
 
 /-! ### join -/
 
-@[simp] theorem join_data {l : Array (Array α)} : l.join.data = (l.data.map data).join := by
+@[simp] theorem data_join {l : Array (Array α)} : l.join.data = (l.data.map data).join := by
   dsimp [join]
   simp only [foldl_eq_foldl_data]
   generalize l.data = l
@@ -102,9 +104,10 @@ theorem size_filter_le (p : α → Bool) (l : Array α) :
   induction l with
   | nil => simp
   | cons h => induction h.data <;> simp [*]
+@[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, join_data, List.mem_join, List.mem_map]
+  simp only [mem_def, data_join, List.mem_join, List.mem_map]
   intro l
   constructor
   · rintro ⟨_, ⟨s, m, rfl⟩, h⟩
@@ -114,7 +117,7 @@ theorem mem_join : ∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L 
 
 /-! ### erase -/
 
-@[simp] proof_wanted erase_data [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a
+@[simp] proof_wanted data_erase [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a
 
 /-! ### shrink -/
 
@@ -127,3 +130,22 @@ theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size -
 theorem size_shrink (a : Array α) (n) : (a.shrink n).size = min a.size n := by
   simp [shrink, size_shrink_loop]
   omega
+
+/-! ### map -/
+
+theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
+  rw [mapM, mapM.map]; rfl
+
+@[simp] theorem map_empty (f : α → β) : map f #[] = #[] := mapM_empty ..
+
+/-! ### mem -/
+
+alias not_mem_empty := not_mem_nil
+
+theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
+
+/-! ### append -/
+
+alias append_empty := append_nil
+
+alias empty_append := nil_append

Batteries/Data/Array/Merge.lean

@@ -27,7 +27,7 @@ where
   termination_by xs.size + ys.size - (i + j)
 
 set_option linter.unusedVariables false in
-@[deprecated merge, inherit_doc merge]
+@[deprecated merge (since := "2024-04-24"), inherit_doc merge]
 def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) : Array α :=
   merge (compare · · |>.isLT) xs ys
 
@@ -55,7 +55,7 @@ where
       | .eq => go (acc.push (merge x y)) (i + 1) (j + 1)
   termination_by xs.size + ys.size - (i + j)
 
-@[deprecated] alias mergeSortedMergingDuplicates := mergeDedupWith
+@[deprecated (since := "2024-04-24")] alias mergeSortedMergingDuplicates := mergeDedupWith
 
 /--
 `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
@@ -64,7 +64,7 @@ not contain duplicates. If an element appears in both `xs` and `ys`, only one co
 @[inline] def mergeDedup [ord : Ord α] (xs ys : Array α) : Array α :=
   mergeDedupWith (ord := ord) xs ys fun x _ => x
 
-@[deprecated] alias mergeSortedDeduplicating := mergeDedup
+@[deprecated (since := "2024-04-24")] alias mergeSortedDeduplicating := mergeDedup
 
 set_option linter.unusedVariables false in
 /--
@@ -83,7 +83,7 @@ where
     ys.foldl (init := xs) fun xs y =>
       if xs.any (· == y) (stop := xsSize) then xs else xs.push y
 
-@[deprecated] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
+@[deprecated (since := "2024-04-24")] alias mergeUnsortedDeduplicating := mergeUnsortedDedup
 
 /--
 `O(|xs|)`. Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with
@@ -101,7 +101,7 @@ where
       acc.push hd
   termination_by xs.size - i
 
-@[deprecated] alias mergeAdjacentDuplicates := mergeAdjacentDups
+@[deprecated (since := "2024-04-24")] alias mergeAdjacentDuplicates := mergeAdjacentDups
 
 /--
 `O(|xs|)`. Deduplicate a sorted array. The array must be sorted with to an order which agrees with
@@ -110,13 +110,13 @@ where
 def dedupSorted [eq : BEq α] (xs : Array α) : Array α :=
   xs.mergeAdjacentDups (eq := eq) fun x _ => x
 
-@[deprecated] alias deduplicateSorted := dedupSorted
+@[deprecated (since := "2024-04-24")] alias deduplicateSorted := dedupSorted
 
 /-- `O(|xs| log |xs|)`. Sort and deduplicate an array. -/
 def sortDedup [ord : Ord α] (xs : Array α) : Array α :=
   have := ord.toBEq
   dedupSorted <| xs.qsort (compare · · |>.isLT)
 
-@[deprecated] alias sortAndDeduplicate := sortDedup
+@[deprecated (since := "2024-04-24")] alias sortAndDeduplicate := sortDedup
 
 end Array