From 1d25ec7ec98d6d9fb526c997aa014bcabbad8b72 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Tue, 13 Aug 2024 15:34:09 -0400
Subject: [PATCH] fix: naming convention (#914)

Many theorems have the reverse naming convention for `Array.data` and `ByteArray.data`. This fixes many of them but there are plenty more in Lean core. An unexpected upshot is that some corrected names are actually shorter!
---
 Batteries/Data/Array/Lemmas.lean | 20 +++++++++++--------
 Batteries/Data/ByteArray.lean    | 33 ++++++++++++++++++++------------
 2 files changed, 33 insertions(+), 20 deletions(-)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index 753cbb4955..dd4fe12424 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/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 →
@@ -27,10 +27,11 @@ theorem forIn_eq_data_forIn [Monad m]
       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
@@ -70,14 +71,16 @@ theorem zipWith_eq_zipWith_data (f : α → β → γ) (as : Array α) (bs : Arr
         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]
   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 :=
@@ -92,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
@@ -101,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⟩
@@ -113,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 -/
 
diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
index 585563ec5a..a9653bf10c 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
+import Batteries.Tactic.Alias
 
 namespace ByteArray
 
@@ -18,15 +19,18 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
 
 /-! ### empty -/
 
-@[simp] theorem mkEmpty_data (cap) : (mkEmpty cap).data = #[] := rfl
+@[simp] theorem data_mkEmpty (cap) : (mkEmpty cap).data = #[] := rfl
+@[deprecated (since := "2024-08-13")] alias mkEmpty_data := data_mkEmpty
 
-@[simp] theorem empty_data : empty.data = #[] := rfl
+@[simp] theorem data_empty : empty.data = #[] := rfl
+@[deprecated (since := "2024-08-13")] alias empty_data := data_empty
 
 @[simp] theorem size_empty : empty.size = 0 := rfl
 
 /-! ### push -/
 
-@[simp] theorem push_data (a : ByteArray) (b : UInt8) : (a.push b).data = a.data.push b := rfl
+@[simp] theorem data_push (a : ByteArray) (b : UInt8) : (a.push b).data = a.data.push b := rfl
+@[deprecated (since := "2024-08-13")] alias push_data := data_push
 
 @[simp] theorem size_push (a : ByteArray) (b : UInt8) : (a.push b).size = a.size + 1 :=
   Array.size_push ..
@@ -40,8 +44,9 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
 
 /-! ### set -/
 
-@[simp] theorem set_data (a : ByteArray) (i : Fin a.size) (v : UInt8) :
+@[simp] theorem data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
     (a.set i v).data = a.data.set i v := rfl
+@[deprecated (since := "2024-08-13")] alias set_data := data_set
 
 @[simp] theorem size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
     (a.set i v).size = a.size :=
@@ -60,20 +65,22 @@ theorem set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) :
 
 /-! ### copySlice -/
 
-@[simp] theorem copySlice_data (a i b j len exact) :
+@[simp] theorem data_copySlice (a i b j len exact) :
   (copySlice a i b j len exact).data = b.data.extract 0 j ++ a.data.extract i (i + len)
     ++ b.data.extract (j + min len (a.data.size - i)) b.data.size := rfl
+@[deprecated (since := "2024-08-13")] alias copySlice_data := data_copySlice
 
 /-! ### append -/
 
 @[simp] theorem append_eq (a b) : ByteArray.append a b = a ++ b := rfl
 
-@[simp] theorem append_data (a b : ByteArray) : (a ++ b).data = a.data ++ b.data := by
+@[simp] theorem data_append (a b : ByteArray) : (a ++ b).data = a.data ++ b.data := by
   rw [←append_eq]; simp [ByteArray.append, size]
   rw [Array.extract_empty_of_stop_le_start (h:=Nat.le_add_right ..), Array.append_nil]
+@[deprecated (since := "2024-08-13")] alias append_data := data_append
 
 theorem size_append (a b : ByteArray) : (a ++ b).size = a.size + b.size := by
-  simp only [size, append_eq, append_data]; exact Array.size_append ..
+  simp only [size, append_eq, data_append]; exact Array.size_append ..
 
 theorem get_append_left {a b : ByteArray} (hlt : i < a.size)
     (h : i < (a ++ b).size := size_append .. ▸ Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)) :
@@ -87,12 +94,13 @@ theorem get_append_right {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b
 
 /-! ### extract -/
 
-@[simp] theorem extract_data (a : ByteArray) (start stop) :
+@[simp] theorem data_extract (a : ByteArray) (start stop) :
     (a.extract start stop).data = a.data.extract start stop := by
   simp [extract]
   match Nat.le_total start stop with
   | .inl h => simp [h, Nat.add_sub_cancel']
   | .inr h => simp [h, Nat.sub_eq_zero_of_le, Array.extract_empty_of_stop_le_start]
+@[deprecated (since := "2024-08-13")] alias extract_data := data_extract
 
 @[simp] theorem size_extract (a : ByteArray) (start stop) :
     (a.extract start stop).size = min stop a.size - start := by
@@ -113,7 +121,8 @@ theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start s
 def ofFn (f : Fin n → UInt8) : ByteArray where
   data := .ofFn f
 
-@[simp] theorem ofFn_data (f : Fin n → UInt8) : (ofFn f).data = .ofFn f := rfl
+@[simp] theorem data_ofFn (f : Fin n → UInt8) : (ofFn f).data = .ofFn f := rfl
+@[deprecated (since := "2024-08-13")] alias ofFn_data := data_ofFn
 
 @[simp] theorem size_ofFn (f : Fin n → UInt8) : (ofFn f).size = n := by
   simp [size]
@@ -131,9 +140,9 @@ private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where
 termination_by n - i
 
 @[csimp] private theorem ofFn_eq_ofFnAux : @ofFn = @ofFnAux := by
-  funext n f; ext; simp [ofFnAux, Array.ofFn, ofFnAux_data, mkEmpty]
+  funext n f; ext; simp [ofFnAux, Array.ofFn, data_ofFnAux, mkEmpty]
 where
-  ofFnAux_data {n} (f : Fin n → UInt8) (i) {acc} :
+  data_ofFnAux {n} (f : Fin n → UInt8) (i) {acc} :
       (ofFnAux.go f i acc).data = Array.ofFn.go f i acc.data := by
-    rw [ofFnAux.go, Array.ofFn.go]; split; rw [ofFnAux_data f (i+1), push_data]; rfl
+    rw [ofFnAux.go, Array.ofFn.go]; split; rw [data_ofFnAux f (i+1), data_push]; rfl
   termination_by n - i