feat: add Data.Fin.Coding and Data.Fin.Enum

Batteries/Data/Fin.lean

@@ -1,2 +1,4 @@
 import Batteries.Data.Fin.Basic
+import Batteries.Data.Fin.Coding
+import Batteries.Data.Fin.Enum
 import Batteries.Data.Fin.Lemmas

Batteries/Data/Fin/Basic.lean

@@ -68,3 +68,43 @@ Fin.foldrM n f xₙ = do
   loop : {i // i ≤ n} → α → m α
   | ⟨0, _⟩, x => pure x
   | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩
+
+/-- Sum of a list indexed by `Fin n`. -/
+protected def sum [OfNat α (nat_lit 0)] [Add α] (x : Fin n → α) : α :=
+  foldr n (x · + ·) 0
+
+/-- Product of a list indexed by `Fin n`. -/
+protected def prod [OfNat α (nat_lit 1)] [Mul α] (x : Fin n → α) : α :=
+  foldr n (x · * ·) 1
+
+/-- Count the number of true values of a decidable predicate on `Fin n`. -/
+protected def count (P : Fin n → Prop) [DecidablePred P] : Nat :=
+  Fin.sum (if P · then 1 else 0)
+
+/-- Find the first true value of a decidable predicate on `Fin n`, if there is one. -/
+protected def find? (P : Fin n → Prop) [inst : DecidablePred P] : Option (Fin n) :=
+  match n, P, inst with
+  | 0, _, _ => none
+  | _+1, P, _ =>
+    if P 0 then
+      some 0
+    else
+      match Fin.find? fun i => P i.succ with
+      | some i => some i.succ
+      | none => none
+
+/-- Custom recursor for `Fin (n+1)`. -/
+def recZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1))
+    (zero : motive 0) (succ : (x : Fin n) → motive x.castSucc → motive x.succ) : motive x :=
+  match x with
+  | 0 => zero
+  | ⟨x+1, hx⟩ =>
+    let x : Fin n := ⟨x, Nat.lt_of_succ_lt_succ hx⟩
+    succ x <| recZeroSuccOn x.castSucc zero succ
+
+/-- Custom recursor for `Fin (n+1)`. -/
+def casesZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1))
+    (zero : motive 0) (succ : (x : Fin n) → motive x.succ) : motive x :=
+  match x with
+  | 0 => zero
+  | ⟨x+1, hx⟩ => succ ⟨x, Nat.lt_of_succ_lt_succ hx⟩