From 299be2f00ba744dd0dbb44d393e537082786fb73 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Mon, 20 Nov 2023 01:30:38 -0500 Subject: [PATCH] feat: `Fin.foldl` and `Fin.foldr` (#374) Co-authored-by: Scott Morrison Co-authored-by: Mario Carneiro --- Std/Data/Fin/Basic.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Std/Data/Fin/Basic.lean b/Std/Data/Fin/Basic.lean index 2710b383fe..f7f3f112af 100644 --- a/Std/Data/Fin/Basic.lean +++ b/Std/Data/Fin/Basic.lean @@ -48,3 +48,17 @@ def natAdd (n) (i : Fin m) : Fin (n + m) := ⟨n + i, Nat.add_lt_add_left i.2 _ /-- `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 ..)⟩ + +/-- 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 loop i => 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)