From 966c7059d35e407dabc4cb862181ba94687402b2 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Sun, 1 Dec 2024 18:45:00 -0700 Subject: [PATCH] defined dependent version of `Fin.foldl` --- Batteries/Data/Fin/Fold.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index ed37c6b948..0ca852f145 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -45,3 +45,21 @@ theorem foldr_eq_foldr_finRange (f : Fin n → α → α) (x) : @[deprecated (since := "2024-11-19")] alias foldr_eq_foldr_list := foldr_eq_foldr_finRange + +variable (n : Nat) (α : Fin (n + 1) → Sort _) + +/-- Dependent version of `Fin.foldl`. -/ +def fold (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := + loop 0 (Nat.zero_lt_succ n) init where + loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α (last n) := + if h' : i < n then + loop (i + 1) (Nat.succ_lt_succ h') (f ⟨i, h'⟩ x) + else + haveI : ⟨i, h⟩ = last n := by + ext + simp only [val_last] + exact Nat.eq_of_lt_succ_of_not_lt h h' + _root_.cast (congrArg α this) x + termination_by n - i + decreasing_by + exact Nat.sub_add_lt_sub h' (Nat.lt_add_one 0)