refactor: add List.finRange and Array.finRange

Harmonize with Mathlib, renaming Fin.list to List.finRange and Fin.enum to Array.finRange.

Batteries/Data/Array/Basic.lean

@@ -175,6 +175,9 @@ def eraseIdx! (a : Array α) (i : Nat) : Array α :=
     have : Inhabited (Array α) := ⟨a⟩
     panic! s!"index {i} out of bounds"
 
+/-- `finRange n` is the array of all elements of `Fin n` in order. -/
+protected def finRange (n : Nat) : Array (Fin n) := ofFn id
+
 end Array
 
 

Batteries/Data/Array/Lemmas.lean

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Batteries.Data.List.Lemmas
+import Batteries.Data.List.FinRange
 import Batteries.Data.Array.Basic
 import Batteries.Tactic.SeqFocus
 import Batteries.Util.ProofWanted
@@ -240,3 +241,20 @@ theorem getElem_insertAt_eq (as : Array α) (i : Fin (as.size+1)) (v : α)
   rw [get_insertAt_loop_eq, Fin.getElem_fin, getElem_push_eq]
   exact heq
   exact Nat.le_of_lt_succ i.is_lt
+
+/-! ### ofFn -/
+
+@[simp] theorem toList_ofFn (f : Fin n → α) : (ofFn f).toList = List.ofFn f := by
+  apply List.ext_getElem <;> simp
+
+/-! ### finRange -/
+
+@[simp] theorem size_finRange (n) : (Array.finRange n).size = n := by
+  simp [Array.finRange]
+
+@[simp] theorem getElem_finRange (n i) (h : i < (Array.finRange n).size) :
+    (Array.finRange n)[i] = ⟨i, size_finRange n ▸ h⟩ := by
+  simp [Array.finRange]
+
+@[simp] theorem toList_finRange (n) : (Array.finRange n).toList = List.finRange n := by
+  simp [Array.finRange, List.finRange]

Batteries/Data/Fin.lean

@@ -1,2 +1,3 @@
 import Batteries.Data.Fin.Basic
+import Batteries.Data.Fin.Fold
 import Batteries.Data.Fin.Lemmas

Batteries/Data/Fin/Basic.lean

@@ -3,17 +3,20 @@ Copyright (c) 2017 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
+import Batteries.Tactic.Alias
+import Batteries.Data.Array.Basic
+import Batteries.Data.List.Basic
 
 namespace Fin
 
 /-- `min n m` as an element of `Fin (m + 1)` -/
 def clamp (n m : Nat) : Fin (m + 1) := ⟨min n m, Nat.lt_succ_of_le (Nat.min_le_right ..)⟩
 
-/-- `enum n` is the array of all elements of `Fin n` in order -/
-def enum (n) : Array (Fin n) := Array.ofFn id
+@[deprecated (since := "2024-11-15")]
+alias enum := Array.finRange
 
-/-- `list n` is the list of all elements of `Fin n` in order -/
-def list (n) : List (Fin n) := (enum n).toList
+@[deprecated (since := "2024-11-15")]
+alias list := List.finRange
 
 /--
 Folds a monadic function over `Fin n` from left to right:

Batteries/Data/Fin/Fold.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 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.Data.List.FinRange
+
+namespace Fin
+
+theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x) :
+    foldlM n f x = (List.finRange n).foldlM f x := by
+  induction n generalizing x with
+  | zero => simp
+  | succ n ih =>
+    rw [foldlM_succ, List.finRange_succ, List.foldlM_cons]
+    congr; funext
+    rw [List.foldlM_map, ih]
+
+@[deprecated (since := "2024-11-19")]
+alias foldlM_eq_foldlM_list := foldlM_eq_foldlM_finRange
+
+theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x) :
+    foldrM n f x = (List.finRange n).foldrM f x := by
+  induction n with
+  | zero => simp
+  | succ n ih => rw [foldrM_succ, ih, List.finRange_succ, List.foldrM_cons, List.foldrM_map]
+
+@[deprecated (since := "2024-11-19")]
+alias foldrM_eq_foldrM_list := foldrM_eq_foldrM_finRange
+
+theorem foldl_eq_foldl_finRange (f : α → Fin n → α) (x) :
+    foldl n f x = (List.finRange n).foldl f x := by
+  induction n generalizing x with
+  | zero => rw [foldl_zero, List.finRange_zero, List.foldl_nil]
+  | succ n ih => rw [foldl_succ, ih, List.finRange_succ, List.foldl_cons, List.foldl_map]
+
+@[deprecated (since := "2024-11-19")]
+alias foldl_eq_foldl_list := foldl_eq_foldl_finRange
+
+theorem foldr_eq_foldr_finRange (f : Fin n → α → α) (x) :
+    foldr n f x = (List.finRange n).foldr f x := by
+  induction n with
+  | zero => rw [foldr_zero, List.finRange_zero, List.foldr_nil]
+  | succ n ih => rw [foldr_succ, ih, List.finRange_succ, List.foldr_cons, List.foldr_map]
+
+@[deprecated (since := "2024-11-19")]
+alias foldr_eq_foldr_list := foldr_eq_foldr_finRange

Batteries/Data/Fin/Lemmas.lean

@@ -14,46 +14,6 @@ attribute [norm_cast] val_last
 
 @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl
 
-/-! ### enum/list -/
-
-@[simp] theorem size_enum (n) : (enum n).size = n := Array.size_ofFn ..
-
-@[simp] theorem enum_zero : (enum 0) = #[] := by simp [enum, Array.ofFn, Array.ofFn.go]
-
-@[simp] theorem getElem_enum (i) (h : i < (enum n).size) : (enum n)[i] = ⟨i, size_enum n ▸ h⟩ :=
-  Array.getElem_ofFn ..
-
-@[simp] theorem length_list (n) : (list n).length = n := by simp [list]
-
-@[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_getElem_toList, 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
-  simp [getElem_list]
-
-@[simp] theorem list_zero : list 0 = [] := by simp [list]
-
-theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
-  apply List.ext_get; simp; intro i; cases i <;> simp
-
-theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
-  rw [list_succ]
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    rw [list_succ, List.map_cons castSucc, ih]
-    simp [Function.comp_def, succ_castSucc]
-
-theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    conv => lhs; rw [list_succ_last]
-    conv => rhs; rw [list_succ]
-    simp [← List.map_reverse, ih, Function.comp_def, rev_succ]
-
 /-! ### foldlM -/
 
 theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
@@ -82,15 +42,6 @@ termination_by n - i
 theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) (x) :
     foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop ..
 
-theorem foldlM_eq_foldlM_list [Monad m] (f : α → Fin n → m α) (x) :
-    foldlM n f x = (list n).foldlM f x := by
-  induction n generalizing x with
-  | zero => simp
-  | succ n ih =>
-    rw [foldlM_succ, list_succ, List.foldlM_cons]
-    congr; funext
-    rw [List.foldlM_map, ih]
-
 /-! ### foldrM -/
 
 theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) :
@@ -119,12 +70,6 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
 theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) :
     foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
 
-theorem foldrM_eq_foldrM_list [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x) :
-    foldrM n f x = (list n).foldrM f x := by
-  induction n with
-  | zero => simp
-  | succ n ih => rw [foldrM_succ, ih, list_succ, List.foldrM_cons, List.foldrM_map]
-
 /-! ### foldl -/
 
 theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) :
@@ -162,11 +107,6 @@ theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
     foldl n f x = foldlM (m:=Id) n f x := by
   induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
 
-theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list n).foldl f x := by
-  induction n generalizing x with
-  | zero => rw [foldl_zero, list_zero, List.foldl_nil]
-  | succ n ih => rw [foldl_succ, ih, list_succ, List.foldl_cons, List.foldl_map]
-
 /-! ### foldr -/
 
 theorem foldr_loop_zero (f : Fin n → α → α) (x) :
@@ -198,11 +138,6 @@ theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
     foldr n f x = foldrM (m:=Id) n f x := by
   induction n <;> simp [foldr_succ, foldrM_succ, *]
 
-theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list n).foldr f x := by
-  induction n with
-  | zero => rw [foldr_zero, list_zero, List.foldr_nil]
-  | succ n ih => rw [foldr_succ, ih, list_succ, List.foldr_cons, List.foldr_map]
-
 theorem foldl_rev (f : Fin n → α → α) (x) :
     foldl n (fun x i => f i.rev x) x = foldr n f x := by
   induction n generalizing x with

Batteries/Data/List.lean

@@ -1,6 +1,7 @@
 import Batteries.Data.List.Basic
 import Batteries.Data.List.Count
 import Batteries.Data.List.EraseIdx
+import Batteries.Data.List.FinRange
 import Batteries.Data.List.Init.Lemmas
 import Batteries.Data.List.Lemmas
 import Batteries.Data.List.Monadic

Batteries/Data/List/Basic.lean

@@ -1064,3 +1064,6 @@ where
   loop : List α → List α → List α
   | [], r => reverseAux (a :: r) [] -- Note: `reverseAux` is tail recursive.
   | b :: l, r => bif p b then reverseAux (a :: r) (b :: l) else loop l (b :: r)
+
+/-- `finRange n` lists all elements of `Fin n` in order -/
+def finRange (n : Nat) : List (Fin n) := ofFn id

Batteries/Data/List/FinRange.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2024 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.Data.List.OfFn
+
+namespace List
+
+@[simp] theorem length_finRange (n) : (List.finRange n).length = n := by
+  simp [List.finRange]
+
+@[deprecated (since := "2024-11-19")]
+alias length_list := length_finRange
+
+@[simp] theorem getElem_finRange (i : Nat) (h : i < (List.finRange n).length) :
+    (finRange n)[i] = Fin.cast (length_finRange n) ⟨i, h⟩ := by
+  simp [List.finRange]
+
+@[deprecated (since := "2024-11-19")]
+alias getElem_list := getElem_finRange
+
+@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn]
+
+@[deprecated (since := "2024-11-19")]
+alias list_zero := finRange_zero
+
+theorem finRange_succ (n) : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
+  apply List.ext_getElem; simp; intro i; cases i <;> simp
+
+@[deprecated (since := "2024-11-19")]
+alias list_succ := finRange_succ
+
+theorem finRange_succ_last (n) :
+    finRange (n+1) = (finRange n).map Fin.castSucc ++ [Fin.last n] := by
+  apply List.ext_getElem
+  · simp
+  · intros
+    simp only [List.finRange, List.getElem_ofFn, getElem_append, length_map, length_ofFn,
+      getElem_map, Fin.castSucc_mk, getElem_singleton]
+    split
+    · rfl
+    · next h => exact Fin.eq_last_of_not_lt h
+
+@[deprecated (since := "2024-11-19")]
+alias list_succ_last := finRange_succ_last
+
+theorem finRange_reverse (n) : (finRange n).reverse = (finRange n).map Fin.rev := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    conv => lhs; rw [finRange_succ_last]
+    conv => rhs; rw [finRange_succ]
+    rw [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, ← map_reverse,
+      map_cons, ih, map_map, map_map]
+    congr; funext
+    simp [Fin.rev_succ]
+
+@[deprecated (since := "2024-11-19")]
+alias list_reverse := finRange_reverse