feat: complete aligning List/Array/Vector.finRange (#7106)

This PR completes the alignment of `List/Array/Vector.finRange` lemmas.

src/Init/Data/Array/FinRange.lean

@@ -5,10 +5,43 @@ Authors: François G. Dorais
 -/
 prelude
 import Init.Data.List.FinRange
+import Init.Data.Array.OfFn
 
 namespace Array
 
 /-- `finRange n` is the array of all elements of `Fin n` in order. -/
 protected def finRange (n : Nat) : Array (Fin n) := ofFn fun i => i
 
+@[simp] theorem size_finRange (n) : (Array.finRange n).size = n := by
+  simp [Array.finRange]
+
+@[simp] theorem getElem_finRange (i : Nat) (h : i < (Array.finRange n).size) :
+    (Array.finRange n)[i] = Fin.cast (size_finRange n) ⟨i, h⟩ := by
+  simp [Array.finRange]
+
+@[simp] theorem finRange_zero : Array.finRange 0 = #[] := by simp [Array.finRange]
+
+theorem finRange_succ (n) : Array.finRange (n+1) = #[0] ++ (Array.finRange n).map Fin.succ := by
+  ext
+  · simp [Nat.add_comm]
+  · simp [getElem_append]
+    split <;>
+    · simp; omega
+
+theorem finRange_succ_last (n) :
+    Array.finRange (n+1) = (Array.finRange n).map Fin.castSucc ++ #[Fin.last n] := by
+  ext
+  · simp
+  · simp [getElem_push]
+    split
+    · simp
+    · simp_all
+      omega
+
+theorem finRange_reverse (n) : (Array.finRange n).reverse = (Array.finRange n).map Fin.rev := by
+  ext i h
+  · simp
+  · simp
+    omega
+
 end Array

src/Init/Data/Vector.lean

@@ -16,4 +16,5 @@ import Init.Data.Vector.Range
 import Init.Data.Vector.Erase
 import Init.Data.Vector.Monadic
 import Init.Data.Vector.InsertIdx
+import Init.Data.Vector.FinRange
 import Init.Data.Vector.Extract

src/Init/Data/Vector/FinRange.lean

@@ -0,0 +1,42 @@
+/-
+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
+-/
+prelude
+import Init.Data.Array.FinRange
+import Init.Data.Vector.OfFn
+
+namespace Vector
+
+/-- `finRange n` is the vector of all elements of `Fin n` in order. -/
+protected def finRange (n : Nat) : Vector (Fin n) n := ofFn fun i => i
+
+@[simp] theorem getElem_finRange (i : Nat) (h : i < n) :
+    (Vector.finRange n)[i] = ⟨i, h⟩ := by
+  simp [Vector.finRange]
+
+@[simp] theorem finRange_zero : Vector.finRange 0 = #v[] := by simp [Vector.finRange]
+
+theorem finRange_succ (n) : Vector.finRange (n+1) =
+    (#v[(0 : Fin (n+1))] ++ (Vector.finRange n).map Fin.succ).cast (by omega) := by
+  ext i h
+  · simp [getElem_append]
+    split <;>
+    · simp; omega
+
+theorem finRange_succ_last (n) :
+    Vector.finRange (n+1) = (Vector.finRange n).map Fin.castSucc ++ #v[Fin.last n] := by
+  ext i h
+  · simp [getElem_push]
+    split
+    · simp
+    · simp_all
+      omega
+
+theorem finRange_reverse (n) : (Vector.finRange n).reverse = (Vector.finRange n).map Fin.rev := by
+  ext i h
+  simp
+  omega
+
+end Vector