From b41499cec176998c92a3eec3598ed7d67717b913 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Mon, 19 Feb 2024 13:16:17 +1100
Subject: [PATCH] chore: upstream Std.Data.Fin.Basic (#3390)

---
 src/Init/Data/Fin.lean       |  1 +
 src/Init/Data/Fin/Basic.lean | 41 +++++++++++++++++++++++++++++++++++-
 src/Init/Data/Fin/Fold.lean  | 21 ++++++++++++++++++
 3 files changed, 62 insertions(+), 1 deletion(-)
 create mode 100644 src/Init/Data/Fin/Fold.lean

diff --git a/src/Init/Data/Fin.lean b/src/Init/Data/Fin.lean
index 82be0e017f..fadf98a9d9 100644
--- a/src/Init/Data/Fin.lean
+++ b/src/Init/Data/Fin.lean
@@ -6,3 +6,4 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Fin.Log2
+import Init.Data.Fin.Fold
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 937d4dc6f8..e5b44aab68 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
+Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Div
@@ -117,6 +117,45 @@ theorem modn_lt : ∀ {m : Nat} (i : Fin n), m > 0 → (modn i m).val < m
 theorem val_lt_of_le (i : Fin b) (h : b ≤ n) : i.val < n :=
   Nat.lt_of_lt_of_le i.isLt h
 
+protected theorem pos (i : Fin n) : 0 < n :=
+  Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
+
+/-- The greatest value of `Fin (n+1)`. -/
+@[inline] def last (n : Nat) : Fin (n + 1) := ⟨n, n.lt_succ_self⟩
+
+/-- `castLT i h` embeds `i` into a `Fin` where `h` proves it belongs into.  -/
+@[inline] def castLT (i : Fin m) (h : i.1 < n) : Fin n := ⟨i.1, h⟩
+
+/-- `castLE h i` embeds `i` into a larger `Fin` type.  -/
+@[inline] def castLE (h : n ≤ m) (i : Fin n) : Fin m := ⟨i, Nat.lt_of_lt_of_le i.2 h⟩
+
+/-- `cast eq i` embeds `i` into an equal `Fin` type. -/
+@[inline] def cast (eq : n = m) (i : Fin n) : Fin m := ⟨i, eq ▸ i.2⟩
+
+/-- `castAdd m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAdd` and `Fin.addNat`. -/
+@[inline] def castAdd (m) : Fin n → Fin (n + m) :=
+  castLE <| Nat.le_add_right n m
+
+/-- `castSucc i` embeds `i : Fin n` in `Fin (n+1)`. -/
+@[inline] def castSucc : Fin n → Fin (n + 1) := castAdd 1
+
+/-- `addNat m i` adds `m` to `i`, generalizes `Fin.succ`. -/
+def addNat (i : Fin n) (m) : Fin (n + m) := ⟨i + m, Nat.add_lt_add_right i.2 _⟩
+
+/-- `natAdd n i` adds `n` to `i` "on the left". -/
+def natAdd (n) (i : Fin m) : Fin (n + m) := ⟨n + i, Nat.add_lt_add_left i.2 _⟩
+
+/-- Maps `0` to `n-1`, `1` to `n-2`, ..., `n-1` to `0`. -/
+@[inline] def rev (i : Fin n) : Fin n := ⟨n - (i + 1), Nat.sub_lt i.pos (Nat.succ_pos _)⟩
+
+/-- `subNat i h` subtracts `m` from `i`, generalizes `Fin.pred`. -/
+@[inline] def subNat (m) (i : Fin (n + m)) (h : m ≤ i) : Fin n :=
+  ⟨i - m, Nat.sub_lt_right_of_lt_add h i.2⟩
+
+/-- Predecessor of a nonzero element of `Fin (n+1)`. -/
+@[inline] def pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n :=
+  subNat 1 i <| Nat.pos_of_ne_zero <| mt (Fin.eq_of_val_eq (j := 0)) h
+
 end Fin
 
 instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean
new file mode 100644
index 0000000000..fcca12fedc
--- /dev/null
+++ b/src/Init/Data/Fin/Fold.lean
@@ -0,0 +1,21 @@
+/-
+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
+-/
+prelude
+import Init.Data.Nat.Linear
+
+/-- Folds over `Fin n` from the left: `foldl 3 f x = f (f (f x 0) 1) 2`. -/
+@[inline] def foldl (n) (f : α → Fin n → α) (init : α) : α := loop init 0 where
+  /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
+  loop (x : α) (i : Nat) : α :=
+    if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
+  termination_by n - i
+
+/-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
+@[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where
+  /-- Inner loop for `Fin.foldr`. `Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))`  -/
+  loop : {i // i ≤ n} → α → α
+  | ⟨0, _⟩, x => x
+  | ⟨i+1, h⟩, x => loop ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x)