Merge branch 'main' into erase_data

.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,6 +14,7 @@ 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
@@ -35,6 +35,7 @@ import Batteries.Data.Range
 import Batteries.Data.Rat
 import Batteries.Data.String
 import Batteries.Data.Sum
+import Batteries.Data.Thunk
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
 import Batteries.Lean.AttributeExtra
@@ -57,18 +58,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
@@ -100,7 +98,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

Batteries/CodeAction/Deprecated.lean

@@ -32,7 +32,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

@@ -22,7 +22,7 @@ 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]
@@ -64,12 +64,11 @@ 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)]
 
 theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
@@ -182,3 +181,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