Trigger CI for leanprover/lean4#3714

Batteries.lean

@@ -16,21 +16,17 @@ 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
 import Batteries.Data.FloatArray
 import Batteries.Data.HashMap
-import Batteries.Data.Int
 import Batteries.Data.LazyList
 import Batteries.Data.List
 import Batteries.Data.MLList
 import Batteries.Data.Nat
-import Batteries.Data.Option
 import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range

Batteries/Data/Array/Lemmas.lean

@@ -11,30 +11,33 @@ import Batteries.Util.ProofWanted
 
 namespace Array
 
-theorem forIn_eq_forIn_data [Monad m]
+theorem forIn_eq_forIn_toList [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn as b f = forIn as.data b f := by
+    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.data.drop j) b f
+      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.data.drop (j + 1) = as.data.drop j := by
+      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
+
+@[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
 
 /-! ### zipWith / zip -/
 
-theorem data_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
-    (as.zipWith bs f).data = as.data.zipWith f bs.data := by
+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).data = cs.data ++ (as.data.drop i).zipWith f (bs.data.drop i) := by
+      (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
@@ -59,27 +62,30 @@ theorem data_zipWith (f : α → β → γ) (as : Array α) (bs : Array β) :
       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_data]
+      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.data.length := ⟨i, has⟩
-      let i_bs : Fin bs.data.length := ⟨i, hbs⟩
+      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_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 [data_length, Fin.getElem_fin, List.getElem_cons_drop, List.get_eq_getElem]
+      rw [← List.zipWith_append (h := by simp), getElem_eq_toList_getElem,
+        getElem_eq_toList_getElem]
+      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 [toList_length, 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
 
 theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by
-  rw [size_eq_length_data, data_zipWith, List.length_zipWith]
+  rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]
 
-theorem data_zip (as : Array α) (bs : Array β) :
-    (as.zip bs).data = as.data.zip bs.data :=
-  data_zipWith Prod.mk as bs
+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
 
 theorem size_zip (as : Array α) (bs : Array β) :
@@ -90,34 +96,36 @@ theorem size_zip (as : Array α) (bs : Array β) :
 
 theorem size_filter_le (p : α → Bool) (l : Array α) :
     (l.filter p).size ≤ l.size := by
-  simp only [← data_length, filter_data]
+  simp only [← toList_length, filter_toList]
   apply List.length_filter_le
 
 /-! ### join -/
 
-@[simp] theorem data_join {l : Array (Array α)} : l.join.data = (l.data.map data).join := by
+@[simp] theorem toList_join {l : Array (Array α)} : l.join.toList = (l.toList.map toList).join := by
   dsimp [join]
-  simp only [foldl_eq_foldl_data]
-  generalize l.data = l
-  have : ∀ a : Array α, (List.foldl ?_ a l).data = a.data ++ ?_ := ?_
+  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.data <;> 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, data_join, List.mem_join, List.mem_map]
+  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.data, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
+    refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩
 
 /-! ### erase -/
 
-@[simp] proof_wanted data_erase [BEq α] {l : Array α} {a : α} : (l.erase a).data = l.data.erase a
+@[simp] proof_wanted toList_erase [BEq α] {l : Array α} {a : α} :
+    (l.erase a).toList = l.toList.erase a
 
 /-! ### shrink -/
 
@@ -145,8 +153,6 @@ theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
 
 /-! ### mem -/
 
-alias not_mem_empty := not_mem_nil
-
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
 /-! ### append -/

Batteries/Data/Array/Pairwise.lean

@@ -17,15 +17,15 @@ larger indices.
 For example `as.Pairwise (· ≠ ·)` asserts that `as` has no duplicates, `as.Pairwise (· < ·)` asserts
 that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is weakly sorted.
 -/
-def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.data.Pairwise R
+def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R
 
 theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Fin as.size), i < j → R (as.get i) (as.get j) := by
-  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_data_get]; rfl
+  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_toList_get]; rfl
 
 theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Nat) (_ : i < as.size) (_ : j < as.size), i < j → R as[i] as[j] := by
-  unfold Pairwise; simp [List.pairwise_iff_getElem, data_length]; rfl
+  unfold Pairwise; simp [List.pairwise_iff_getElem, toList_length]; rfl
 
 instance (R : α → α → Prop) [DecidableRel R] (as) : Decidable (Pairwise R as) :=
   have : (∀ (j : Fin as.size) (i : Fin j.val), R as[i.val] (as[j.val])) ↔ Pairwise R as := by
@@ -46,12 +46,13 @@ theorem pairwise_pair : #[a, b].Pairwise R ↔ R a b := by
 
 theorem pairwise_append {as bs : Array α} :
     (as ++ bs).Pairwise R ↔ as.Pairwise R ∧ bs.Pairwise R ∧ (∀ x ∈ as, ∀ y ∈ bs, R x y) := by
-  unfold Pairwise; simp [← mem_data, append_data, ← List.pairwise_append]
+  unfold Pairwise; simp [← mem_toList, append_toList, ← List.pairwise_append]
 
 theorem pairwise_push {as : Array α} :
     (as.push a).Pairwise R ↔ as.Pairwise R ∧ (∀ x ∈ as, R x a) := by
   unfold Pairwise
-  simp [← mem_data, push_data, List.pairwise_append, List.pairwise_singleton, List.mem_singleton]
+  simp [← mem_toList, push_toList, List.pairwise_append, List.pairwise_singleton,
+    List.mem_singleton]
 
 theorem pairwise_extract {as : Array α} (h : as.Pairwise R) (start stop) :
     (as.extract start stop).Pairwise R := by

Batteries/Data/AssocList.lean

@@ -78,7 +78,7 @@ def toListTR (as : AssocList α β) : List (α × β) :=
 
 @[csimp] theorem toList_eq_toListTR : @toList = @toListTR := by
   funext α β as; simp [toListTR]
-  exact .symm <| (Array.foldl_data_eq_map (toList as) _ id).trans (List.map_id _)
+  exact .symm <| (Array.foldl_toList_eq_map (toList as) _ id).trans (List.map_id _)
 
 /-- `O(n)`. Run monadic function `f` on all elements in the list, from head to tail. -/
 @[specialize] def forM [Monad m] (f : α → β → m PUnit) : AssocList α β → m PUnit

Batteries/Data/Fin/Basic.lean

@@ -13,4 +13,4 @@ def clamp (n m : Nat) : Fin (m + 1) := ⟨min n m, Nat.lt_succ_of_le (Nat.min_le
 def enum (n) : Array (Fin n) := Array.ofFn id
 
 /-- `list n` is the list of all elements of `Fin n` in order -/
-def list (n) : List (Fin n) := (enum n).data
+def list (n) : List (Fin n) := (enum n).toList

Batteries/Data/Fin/Lemmas.lean

@@ -30,7 +30,7 @@ attribute [norm_cast] val_last
 
 @[simp] theorem getElem_list (i : Nat) (h : i < (list n).length) :
     (list n)[i] = cast (length_list n) ⟨i, h⟩ := by
-  simp only [list]; rw [← Array.getElem_eq_data_getElem, getElem_enum, cast_mk]
+  simp only [list]; rw [← Array.getElem_eq_toList_getElem, getElem_enum, cast_mk]
 
 @[deprecated getElem_list (since := "2024-06-12")]
 theorem get_list (i : Fin (list n).length) : (list n).get i = i.cast (length_list n) := by

Batteries/Data/HashMap/Basic.lean

@@ -37,7 +37,7 @@ def update (data : Buckets α β) (i : USize)
 The number of elements in the bucket array.
 Note: this is marked `noncomputable` because it is only intended for specification.
 -/
-noncomputable def size (data : Buckets α β) : Nat := .sum (data.1.data.map (·.toList.length))
+noncomputable def size (data : Buckets α β) : Nat := .sum (data.1.toList.map (·.toList.length))
 
 @[simp] theorem update_size (self : Buckets α β) (i d h) :
     (self.update i d h).1.size = self.1.size := Array.size_uset ..
@@ -52,7 +52,7 @@ The well-formedness invariant for the bucket array says that every element hashe
 -/
 structure WF [BEq α] [Hashable α] (buckets : Buckets α β) : Prop where
   /-- The elements of a bucket are all distinct according to the `BEq` relation. -/
-  distinct [LawfulHashable α] [PartialEquivBEq α] : ∀ bucket ∈ buckets.1.data,
+  distinct [LawfulHashable α] [PartialEquivBEq α] : ∀ bucket ∈ buckets.1.toList,
     bucket.toList.Pairwise fun a b => ¬(a.1 == b.1)
   /-- Every element in a bucket should hash to its location. -/
   hash_self (i : Nat) (h : i < buckets.1.size) :