From 966c7059d35e407dabc4cb862181ba94687402b2 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Sun, 1 Dec 2024 18:45:00 -0700 Subject: [PATCH 01/14] 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) From ab2beddcc7711e2bb9b36913316678d0907eb5ab Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Sun, 1 Dec 2024 19:45:11 -0700 Subject: [PATCH 02/14] addressed comments --- Batteries/Data/Fin/Fold.lean | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index 0ca852f145..2e5717e40c 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -51,15 +51,10 @@ 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 + /-- Inner loop for `Fin.fold`. `Fin.fold.loop n f x i = f (f (f x i) ...) (n-1)` -/ 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' + haveI : ⟨i, h⟩ = last n := by ext; simp; omega _root_.cast (congrArg α this) x - termination_by n - i - decreasing_by - exact Nat.sub_add_lt_sub h' (Nat.lt_add_one 0) From 4229c1e05828db366e259e0686cd9126a80c06aa Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Sun, 1 Dec 2024 21:21:25 -0700 Subject: [PATCH 03/14] added defs for `foldRev`, `foldM`, and `foldRevM` --- Batteries/Data/Fin/Basic.lean | 67 +++++++++++++++++++++++++++++++++++ Batteries/Data/Fin/Fold.lean | 13 ------- 2 files changed, 67 insertions(+), 13 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index f1357f50b0..94e0b20f1b 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -71,3 +71,70 @@ 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⟩ + +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 + /-- Inner loop for `Fin.fold`. `Fin.fold.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/ + 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; omega + _root_.cast (congrArg α this) x + +/-- Dependent version of `Fin.foldr`. -/ +def foldRev (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := + loop n (Nat.lt_succ_self n) init where + /-- Inner loop for `Fin.foldRev`. + `Fin.foldRev.loop n α f i h x = f 0 (f 1 (... (f i x)))` -/ + loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := + if h' : i > 0 then + loop (i - 1) (by omega) (f ⟨i - 1, by omega⟩ + (by simpa [Nat.sub_one_add_one_eq_of_pos h'] using x)) + else + haveI : ⟨i, h⟩ = 0 := by ext; simp; omega + _root_.cast (congrArg α this) x + +/-- Dependent version of `Fin.foldlM`. -/ +def foldM [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) + : m (α (last n)) := loop 0 (Nat.zero_lt_succ n) init where + /-- Inner loop for `Fin.foldM`. + ``` + Fin.foldM.loop n α f i h xᵢ = do + let xᵢ₊₁ ← f i xᵢ + ... + let xₙ ← f (n-1) xₙ₋₁ + pure xₙ + ``` + -/ + loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α (last n)) := + if h' : i < n then + (f ⟨i, h'⟩ x) >>= loop (i + 1) (Nat.succ_lt_succ h') + else + haveI : ⟨i, h⟩ = last n := by ext; simp; omega + _root_.cast (congrArg (fun i => m (α i)) this) (pure x) + termination_by n - i + +/-- Dependent version of `Fin.foldrM`. -/ +def foldRevM [Monad m] (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) + : m (α 0) := loop n (Nat.lt_succ_self n) init where + /-- Inner loop for `Fin.foldRevM`. + ``` + Fin.foldRevM.loop n α f i h xᵢ = do + let xᵢ₋₁ ← f (i+1) xᵢ + ... + let x₁ ← f 1 x₂ + let x₀ ← f 0 x₁ + pure x₀ + ``` + -/ + loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α 0) := + if h' : i > 0 then + (f ⟨i - 1, by omega⟩ (by simpa [Nat.sub_one_add_one_eq_of_pos h'] using x)) + >>= loop (i - 1) (by omega) + else + haveI : ⟨i, h⟩ = 0 := by ext; simp; omega + _root_.cast (congrArg (fun i => m (α i)) this) (pure x) diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index 2e5717e40c..ed37c6b948 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -45,16 +45,3 @@ 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 - /-- Inner loop for `Fin.fold`. `Fin.fold.loop n f x i = f (f (f x i) ...) (n-1)` -/ - 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; omega - _root_.cast (congrArg α this) x From bd02942d59f88be646f3574509486ab2779c7d39 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Mon, 2 Dec 2024 10:23:27 -0700 Subject: [PATCH 04/14] added lemmas for `foldM` and `fold` --- Batteries/Data/Fin/Basic.lean | 9 ++-- Batteries/Data/Fin/Lemmas.lean | 97 +++++++++++++++++++++++++++++++++- 2 files changed, 99 insertions(+), 7 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 94e0b20f1b..a3fea179de 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -75,7 +75,7 @@ Fin.foldrM n f xₙ = do 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) := +@[inline] def fold (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := loop 0 (Nat.zero_lt_succ n) init where /-- Inner loop for `Fin.fold`. `Fin.fold.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/ loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α (last n) := @@ -86,7 +86,7 @@ def fold (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α ( _root_.cast (congrArg α this) x /-- Dependent version of `Fin.foldr`. -/ -def foldRev (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := +@[inline] def foldRev (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := loop n (Nat.lt_succ_self n) init where /-- Inner loop for `Fin.foldRev`. `Fin.foldRev.loop n α f i h x = f 0 (f 1 (... (f i x)))` -/ @@ -99,7 +99,7 @@ def foldRev (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last _root_.cast (congrArg α this) x /-- Dependent version of `Fin.foldlM`. -/ -def foldM [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) +@[inline] def foldM [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n)) := loop 0 (Nat.zero_lt_succ n) init where /-- Inner loop for `Fin.foldM`. ``` @@ -116,10 +116,9 @@ def foldM [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init else haveI : ⟨i, h⟩ = last n := by ext; simp; omega _root_.cast (congrArg (fun i => m (α i)) this) (pure x) - termination_by n - i /-- Dependent version of `Fin.foldrM`. -/ -def foldRevM [Monad m] (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) +@[inline] def foldRevM [Monad m] (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0) := loop n (Nat.lt_succ_self n) init where /-- Inner loop for `Fin.foldRevM`. ``` diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 90a574cf2c..9a2a73bbfc 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -100,7 +100,7 @@ theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) : foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by rw [foldl_succ] induction n generalizing x with - | zero => simp [foldl_succ, Fin.last] + | zero => simp [foldl_succ, last] | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc] theorem foldl_eq_foldlM (f : α → Fin n → α) (x) : @@ -131,7 +131,7 @@ theorem foldr_succ (f : Fin (n+1) → α → α) (x) : theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) : foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by induction n generalizing x with - | zero => simp [foldr_succ, Fin.last] + | zero => simp [foldr_succ, last] | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc] theorem foldr_eq_foldrM (f : Fin n → α → α) (x) : @@ -149,3 +149,96 @@ theorem foldr_rev (f : α → Fin n → α) (x) : induction n generalizing x with | zero => simp | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ] + +/-! ### foldM -/ + +variable {n : Nat} {α : Fin (n+1) → Type _} [Monad m] + (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) + +theorem foldM_loop_lt (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : + foldM.loop n α f i (Nat.lt_add_right 1 h) x = + (f ⟨i, h⟩ x) >>= (foldM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by + rw [foldM.loop, dif_pos h] + +theorem foldM_loop_eq (x : α ⟨n, Nat.le_refl _⟩) : + foldM.loop n α f n (Nat.le_refl _) x = pure x := by + rw [foldM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] + +@[simp] theorem foldM_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) + (x : α 0) : foldM 0 α f x = pure x := + foldM_loop_eq .. + +variable {α : Fin (n+2) → Type _} (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) + +theorem foldM_loop (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : + foldM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + f ⟨i, h⟩ x >>= (foldM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by + if h' : i < n then + rw [foldM_loop_lt _ h _] + congr; funext + rw [foldM_loop_lt _ h' _, foldM_loop]; rfl + else + cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') + rw [foldM_loop_lt] + congr; funext + rw [foldM_loop_eq, foldM_loop_eq] + +theorem foldM_succ (x) : foldM (n+1) α f x = f 0 x >>= foldM n (α ∘ succ) (f ·.succ ·) := + foldM_loop .. + +/-- Dependent version `foldM` equals non-dependent version `foldlM` --/ +theorem foldM_eq_foldlM {α : Type _} (f : Fin n → α → m α) (x : α) : + foldM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by + induction n generalizing x with + | zero => simp only [foldM_zero, foldlM_zero] + | succ n ih => + simp only [foldM_succ, foldlM_succ, Function.comp_apply, Function.comp_def] + congr; ext; simp only [ih] + +/-! ### fold -/ + +variable {α : Fin (n+1) → Sort _} (f : ∀ (i : Fin n), α i.castSucc → α i.succ) + +theorem fold_loop_lt (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : + fold.loop n α f i (Nat.lt_add_right 1 h) x = + fold.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by + rw [fold.loop, dif_pos h] + +theorem fold_loop_eq (x : α ⟨n, Nat.le_refl _⟩) : + fold.loop n α f n (Nat.le_refl _) x = x := by + rw [fold.loop, dif_neg (Nat.lt_irrefl _), cast_eq] + +@[simp] theorem fold_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.castSucc → α i.succ) + (x : α 0) : fold 0 α f x = x := + fold_loop_eq .. + +variable {α : Fin (n+2) → Sort _} (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) + +theorem fold_loop (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : + fold.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + fold.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by + if h' : i < n then + rw [fold_loop_lt _ h _] + rw [fold_loop_lt _ h' _, fold_loop]; rfl + else + cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') + rw [fold_loop_lt] + rw [fold_loop_eq, fold_loop_eq] + +theorem fold_succ (x : α 0) : fold (n+1) α f x = fold n (α ∘ succ) (f ·.succ ·) (f 0 x) := + fold_loop .. + +theorem fold_succ_last (x : α 0) : + fold (n+1) α f x = f (last n) (fold n (α ∘ castSucc) (f ·.castSucc ·) x) := by + rw [fold_succ] + induction n with + | zero => simp [fold_succ, last] + | succ n ih => rw [fold_succ, @ih (α ∘ succ) (f ·.succ ·), fold_succ]; congr + +theorem fold_eq_foldl {α : Sort _} (f : Fin n → α → α) (x : α) : + fold n (fun _ => α) f x = foldl n (fun x i => f i x) x := by + induction n generalizing x with + | zero => simp only [fold_zero, foldl_zero] + | succ n ih => + simp only [fold_succ, foldl_succ, Function.comp_apply, Function.comp_def] + congr; simp only [ih] From fe135aefac9f66c3b8e46c7dbeb39ef5666a9938 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Mon, 2 Dec 2024 10:44:43 -0700 Subject: [PATCH 05/14] removed materials that have been moved to Lean.Init --- Batteries/Data/Fin/Basic.lean | 54 ------------- Batteries/Data/Fin/Lemmas.lean | 136 --------------------------------- 2 files changed, 190 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index a3fea179de..6408238d55 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -18,60 +18,6 @@ alias enum := Array.finRange @[deprecated (since := "2024-11-15")] alias list := List.finRange -/-- -Folds a monadic function over `Fin n` from left to right: -``` -Fin.foldlM n f x₀ = do - let x₁ ← f x₀ 0 - let x₂ ← f x₁ 1 - ... - let xₙ ← f xₙ₋₁ (n-1) - pure xₙ -``` --/ -@[inline] def foldlM [Monad m] (n) (f : α → Fin n → m α) (init : α) : m α := loop init 0 where - /-- - Inner loop for `Fin.foldlM`. - ``` - Fin.foldlM.loop n f xᵢ i = do - let xᵢ₊₁ ← f xᵢ i - ... - let xₙ ← f xₙ₋₁ (n-1) - pure xₙ - ``` - -/ - loop (x : α) (i : Nat) : m α := do - if h : i < n then f x ⟨i, h⟩ >>= (loop · (i+1)) else pure x - termination_by n - i - -/-- -Folds a monadic function over `Fin n` from right to left: -``` -Fin.foldrM n f xₙ = do - let xₙ₋₁ ← f (n-1) xₙ - let xₙ₋₂ ← f (n-2) xₙ₋₁ - ... - let x₀ ← f 0 x₁ - pure x₀ -``` --/ -@[inline] def foldrM [Monad m] (n) (f : Fin n → α → m α) (init : α) : m α := - loop ⟨n, Nat.le_refl n⟩ init where - /-- - Inner loop for `Fin.foldrM`. - ``` - Fin.foldrM.loop n f i xᵢ = do - let xᵢ₋₁ ← f (i-1) xᵢ - ... - let x₁ ← f 1 x₂ - let x₀ ← f 0 x₁ - pure x₀ - ``` - -/ - loop : {i // i ≤ n} → α → m α - | ⟨0, _⟩, x => pure x - | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩ - variable (n : Nat) (α : Fin (n + 1) → Sort _) /-- Dependent version of `Fin.foldl`. -/ diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 9a2a73bbfc..90de53225b 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -14,142 +14,6 @@ attribute [norm_cast] val_last @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl -/-! ### foldlM -/ - -theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) : - foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by - rw [foldlM.loop, dif_pos h] - -theorem foldlM_loop_eq [Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x := by - rw [foldlM.loop, dif_neg (Nat.lt_irrefl _)] - -theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i < n+1) : - foldlM.loop (n+1) f x i = f x ⟨i, h⟩ >>= (foldlM.loop n (fun x j => f x j.succ) . i) := by - if h' : i < n then - rw [foldlM_loop_lt _ _ h] - congr; funext - rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl - else - cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') - rw [foldlM_loop_lt] - congr; funext - rw [foldlM_loop_eq, foldlM_loop_eq] -termination_by n - i - -@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x := - foldlM_loop_eq .. - -theorem foldlM_succ [Monad m] (f : α → Fin (n+1) → m α) (x) : - foldlM (n+1) f x = f x 0 >>= foldlM n (fun x j => f x j.succ) := foldlM_loop .. - -/-! ### foldrM -/ - -theorem foldrM_loop_zero [Monad m] (f : Fin n → α → m α) (x) : - foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x := by - rw [foldrM.loop] - -theorem foldrM_loop_succ [Monad m] (f : Fin n → α → m α) (x) (h : i < n) : - foldrM.loop n f ⟨i+1, h⟩ x = f ⟨i, h⟩ x >>= foldrM.loop n f ⟨i, Nat.le_of_lt h⟩ := by - rw [foldrM.loop] - -theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) (h : i+1 ≤ n+1) : - foldrM.loop (n+1) f ⟨i+1, h⟩ x = - foldrM.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x >>= f 0 := by - induction i generalizing x with - | zero => - rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind] - conv => rhs; rw [←bind_pure (f 0 x)] - congr; funext; exact foldrM_loop_zero .. - | succ i ih => - rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc] - congr; funext; exact ih .. - -@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x := - foldrM_loop_zero .. - -theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) : - foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop .. - -/-! ### foldl -/ - -theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) : - foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1) := by - rw [foldl.loop, dif_pos h] - -theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x := by - rw [foldl.loop, dif_neg (Nat.lt_irrefl _)] - -theorem foldl_loop (f : α → Fin (n+1) → α) (x) (h : i < n+1) : - foldl.loop (n+1) f x i = foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i := by - if h' : i < n then - rw [foldl_loop_lt _ _ h] - rw [foldl_loop_lt _ _ h', foldl_loop]; rfl - else - cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') - rw [foldl_loop_lt] - rw [foldl_loop_eq, foldl_loop_eq] - -@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x := - foldl_loop_eq .. - -theorem foldl_succ (f : α → Fin (n+1) → α) (x) : - foldl (n+1) f x = foldl n (fun x i => f x i.succ) (f x 0) := - foldl_loop .. - -theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) : - foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by - rw [foldl_succ] - induction n generalizing x with - | zero => simp [foldl_succ, last] - | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc] - -theorem foldl_eq_foldlM (f : α → Fin n → α) (x) : - foldl n f x = foldlM (m:=Id) n f x := by - induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *] - -/-! ### foldr -/ - -theorem foldr_loop_zero (f : Fin n → α → α) (x) : - foldr.loop n f ⟨0, Nat.zero_le _⟩ x = x := by - rw [foldr.loop] - -theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : i < n) : - foldr.loop n f ⟨i+1, h⟩ x = foldr.loop n f ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x) := by - rw [foldr.loop] - -theorem foldr_loop (f : Fin (n+1) → α → α) (x) (h : i+1 ≤ n+1) : - foldr.loop (n+1) f ⟨i+1, h⟩ x = - f 0 (foldr.loop n (fun j => f j.succ) ⟨i, Nat.le_of_succ_le_succ h⟩ x) := by - induction i generalizing x <;> simp [foldr_loop_zero, foldr_loop_succ, *] - -@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x := - foldr_loop_zero .. - -theorem foldr_succ (f : Fin (n+1) → α → α) (x) : - foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop .. - -theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) : - foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by - induction n generalizing x with - | zero => simp [foldr_succ, last] - | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc] - -theorem foldr_eq_foldrM (f : Fin n → α → α) (x) : - foldr n f x = foldrM (m:=Id) n f x := by - induction n <;> simp [foldr_succ, foldrM_succ, *] - -theorem foldl_rev (f : Fin n → α → α) (x) : - foldl n (fun x i => f i.rev x) x = foldr n f x := by - induction n generalizing x with - | zero => simp - | succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ] - -theorem foldr_rev (f : α → Fin n → α) (x) : - foldr n (fun i x => f x i.rev) x = foldl n f x := by - induction n generalizing x with - | zero => simp - | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ] - /-! ### foldM -/ variable {n : Nat} {α : Fin (n+1) → Type _} [Monad m] From 83bca8b81952ad6e409c60439368426b23e358a9 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Mon, 2 Dec 2024 14:39:00 -0700 Subject: [PATCH 06/14] added more lemmas for `foldr{M}` --- Batteries/Data/Fin/Basic.lean | 64 ++++++----- Batteries/Data/Fin/Fold.lean | 204 +++++++++++++++++++++++++++++++++ Batteries/Data/Fin/Lemmas.lean | 93 --------------- 3 files changed, 237 insertions(+), 124 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 6408238d55..2f3be2db65 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -18,36 +18,11 @@ alias enum := Array.finRange @[deprecated (since := "2024-11-15")] alias list := List.finRange -variable (n : Nat) (α : Fin (n + 1) → Sort _) - -/-- Dependent version of `Fin.foldl`. -/ -@[inline] def fold (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := - loop 0 (Nat.zero_lt_succ n) init where - /-- Inner loop for `Fin.fold`. `Fin.fold.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/ - 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; omega - _root_.cast (congrArg α this) x - -/-- Dependent version of `Fin.foldr`. -/ -@[inline] def foldRev (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := - loop n (Nat.lt_succ_self n) init where - /-- Inner loop for `Fin.foldRev`. - `Fin.foldRev.loop n α f i h x = f 0 (f 1 (... (f i x)))` -/ - loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := - if h' : i > 0 then - loop (i - 1) (by omega) (f ⟨i - 1, by omega⟩ - (by simpa [Nat.sub_one_add_one_eq_of_pos h'] using x)) - else - haveI : ⟨i, h⟩ = 0 := by ext; simp; omega - _root_.cast (congrArg α this) x - /-- Dependent version of `Fin.foldlM`. -/ -@[inline] def foldM [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) - : m (α (last n)) := loop 0 (Nat.zero_lt_succ n) init where - /-- Inner loop for `Fin.foldM`. +@[specialize] def dfoldlM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) + (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n)) := + loop 0 (Nat.zero_lt_succ n) init where + /-- Inner loop for `Fin.dfoldlM`. ``` Fin.foldM.loop n α f i h xᵢ = do let xᵢ₊₁ ← f i xᵢ @@ -64,8 +39,9 @@ variable (n : Nat) (α : Fin (n + 1) → Sort _) _root_.cast (congrArg (fun i => m (α i)) this) (pure x) /-- Dependent version of `Fin.foldrM`. -/ -@[inline] def foldRevM [Monad m] (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) - : m (α 0) := loop n (Nat.lt_succ_self n) init where +@[specialize] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) + (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0) := + loop n (Nat.lt_succ_self n) init where /-- Inner loop for `Fin.foldRevM`. ``` Fin.foldRevM.loop n α f i h xᵢ = do @@ -83,3 +59,29 @@ variable (n : Nat) (α : Fin (n + 1) → Sort _) else haveI : ⟨i, h⟩ = 0 := by ext; simp; omega _root_.cast (congrArg (fun i => m (α i)) this) (pure x) + +/-- Dependent version of `Fin.foldl`. -/ +@[specialize] def dfoldl (n : Nat) (α : Fin (n + 1) → Sort _) + (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := + loop 0 (Nat.zero_lt_succ n) init where + /-- Inner loop for `Fin.dfoldl`. `Fin.dfoldl.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/ + 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; omega + _root_.cast (congrArg α this) x + +/-- Dependent version of `Fin.foldr`. -/ +@[specialize] def dfoldr (n : Nat) (α : Fin (n + 1) → Sort _) + (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := + loop n (Nat.lt_succ_self n) init where + /-- Inner loop for `Fin.dfoldr`. + `Fin.dfoldr.loop n α f i h x = f 0 (f 1 (... (f i x)))` -/ + loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := + if h' : i > 0 then + loop (i - 1) (by omega) (f ⟨i - 1, by omega⟩ + (by simpa [Nat.sub_one_add_one_eq_of_pos h'] using x)) + else + haveI : ⟨i, h⟩ = 0 := by ext; simp; omega + _root_.cast (congrArg α this) x diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index ed37c6b948..8bcb1d644a 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -4,9 +4,213 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: François G. Dorais -/ import Batteries.Data.List.FinRange +import Batteries.Data.Fin.Basic namespace Fin +/-! ### dfoldlM -/ + +theorem dfoldlM_loop_lt [Monad m] {n : Nat} {α : Fin (n+1) → Type _} + (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) + (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : + dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x = + (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by + rw [dfoldlM.loop, dif_pos h] + +theorem dfoldlM_loop_eq [Monad m] {n : Nat} {α : Fin (n+1) → Type _} + (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x : α ⟨n, Nat.le_refl _⟩) : + dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by + rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] + +@[simp] theorem dfoldlM_zero [Monad m] {α : Fin 1 → Type _} + (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x : α 0) : + dfoldlM 0 α f x = pure x := + dfoldlM_loop_eq .. + +theorem dfoldlM_loop [Monad m] {n : Nat} {α : Fin (n+2) → Type _} + (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) + (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : + dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by + if h' : i < n then + rw [dfoldlM_loop_lt _ h _] + congr; funext + rw [dfoldlM_loop_lt _ h' _, dfoldlM_loop]; rfl + else + cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') + rw [dfoldlM_loop_lt] + congr; funext + rw [dfoldlM_loop_eq, dfoldlM_loop_eq] + +theorem dfoldlM_succ [Monad m] {n : Nat} {α : Fin (n+2) → Type _} + (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x : α 0) : + dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) := + dfoldlM_loop .. + +/-- Dependent version `dfoldlM` equals non-dependent version `foldlM` -/ +theorem dfoldlM_eq_foldlM [Monad m] {n : Nat} {α : Type _} (f : (i : Fin n) → α → m α) (x : α) : + dfoldlM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by + induction n generalizing x with + | zero => simp only [dfoldlM_zero, foldlM_zero] + | succ n ih => + simp only [dfoldlM_succ, foldlM_succ, Function.comp_apply, Function.comp_def] + congr; ext; simp only [ih] + +/-! ### dfoldrM -/ + +theorem dfoldrM_loop_zero [Monad m] {n : Nat} {α : Fin (n+1) → Type _} + (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α 0) : + dfoldrM.loop n α f 0 (Nat.zero_lt_succ n) x = pure x := by + rw [dfoldrM.loop, dif_neg (Nat.not_lt_zero _), cast_eq] + +theorem dfoldrM_loop_succ [Monad m] {n : Nat} {α : Fin (n+1) → Type _} + (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (h : i < n) + (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : + dfoldrM.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = + f ⟨i, h⟩ x >>= dfoldrM.loop n α f i (Nat.lt_add_right 1 h) := by + rw [dfoldrM.loop, dif_pos (Nat.zero_lt_succ i)] + simp only [Nat.add_one_sub_one, castSucc_mk, succ_mk, eq_mpr_eq_cast, cast_eq] + +theorem dfoldrM_loop [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Type _} + (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) (h : i+1 ≤ n+1) + (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : + dfoldrM.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = + dfoldrM.loop n (α ∘ succ) (f ·.succ) i h x >>= f 0 := by + induction i with + | zero => + rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind] + conv => rhs; rw [←bind_pure (f 0 x)] + congr; funext; exact dfoldrM_loop_zero .. + | succ i ih => + rw [dfoldrM_loop_succ _ h, dfoldrM_loop_succ _ (Nat.succ_lt_succ_iff.mp h), bind_assoc] + congr; funext; exact ih .. + +@[simp] theorem dfoldrM_zero [Monad m] {α : Fin 1 → Type _} + (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x : α 0) : + dfoldrM 0 α f x = pure x := + dfoldrM_loop_zero .. + +theorem dfoldrM_succ [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Type _} + (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) (x : α (last (n+1))) : + dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := + dfoldrM_loop .. + +/-- Dependent version `dfoldrM` equals non-dependent version `foldrM` -/ +theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] {n : Nat} {α : Type _} + (f : (i : Fin n) → α → m α) (x : α) : dfoldrM n (fun _ => α) f x = foldrM n f x := by + induction n generalizing x with + | zero => simp only [dfoldrM_zero, foldrM_zero] + | succ n ih => simp only [dfoldrM_succ, foldrM_succ, Function.comp_def, ih] + +/-! ### dfoldl -/ + +theorem dfoldl_loop_lt {n : Nat} {α : Fin (n+1) → Sort _} + (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : + dfoldl.loop n α f i (Nat.lt_add_right 1 h) x = + dfoldl.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by + rw [dfoldl.loop, dif_pos h] + +theorem dfoldl_loop_eq {n : Nat} {α : Fin (n+1) → Sort _} + (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x : α ⟨n, Nat.le_refl _⟩) : + dfoldl.loop n α f n (Nat.le_refl _) x = x := by + rw [dfoldl.loop, dif_neg (Nat.lt_irrefl _), cast_eq] + +@[simp] theorem dfoldl_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.castSucc → α i.succ) + (x : α 0) : dfoldl 0 α f x = x := + dfoldl_loop_eq .. + +theorem dfoldl_loop {n : Nat} {α : Fin (n+2) → Sort _} + (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) + (x : α ⟨i, Nat.lt_add_right 1 h⟩) : + dfoldl.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + dfoldl.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by + if h' : i < n then + rw [dfoldl_loop_lt _ h _] + rw [dfoldl_loop_lt _ h' _, dfoldl_loop]; rfl + else + cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') + rw [dfoldl_loop_lt] + rw [dfoldl_loop_eq, dfoldl_loop_eq] + +theorem dfoldl_succ {n : Nat} {α : Fin (n+2) → Sort _} + (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : + dfoldl (n+1) α f x = dfoldl n (α ∘ succ) (f ·.succ ·) (f 0 x) := + dfoldl_loop .. + +theorem dfoldl_succ_last {n : Nat} {α : Fin (n+2) → Sort _} + (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : + dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x) := by + rw [dfoldl_succ] + induction n with + | zero => simp [dfoldl_succ, last] + | succ n ih => rw [dfoldl_succ, @ih (α ∘ succ) (f ·.succ ·), dfoldl_succ]; congr + +/-- Dependent version `dfoldl` equals non-dependent version `foldl` -/ +theorem dfoldl_eq_foldl {α : Sort _} (f : Fin n → α → α) (x : α) : + dfoldl n (fun _ => α) f x = foldl n (fun x i => f i x) x := by + induction n generalizing x with + | zero => simp only [dfoldl_zero, foldl_zero] + | succ n ih => + simp only [dfoldl_succ, foldl_succ, Function.comp_apply, Function.comp_def] + congr; simp only [ih] + +/-! ### dfoldr -/ + +theorem dfoldr_loop_zero {n : Nat} {α : Fin (n+1) → Sort _} + (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α 0) : + dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := by + rw [dfoldr.loop, dif_neg (Nat.not_lt_zero _), cast_eq] + +theorem dfoldr_loop_succ {n : Nat} {α : Fin (n+1) → Sort _} + (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) + (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : + dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = + dfoldr.loop n α f i (Nat.lt_add_right 1 h) (f ⟨i, h⟩ x) := by + rw [dfoldr.loop, dif_pos (Nat.zero_lt_succ i)] + simp only [Nat.add_one_sub_one, succ_mk, eq_mpr_eq_cast, cast_eq] + +theorem dfoldr_loop {n : Nat} {α : Fin (n+2) → Sort _} + (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) + (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : + dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = + f 0 (dfoldr.loop n (α ∘ succ) (f ·.succ) i h x) := by + induction i with + | zero => simp [dfoldr_loop_succ, dfoldr_loop_zero] + | succ i ih => rw [dfoldr_loop_succ _ h, dfoldr_loop_succ _ (Nat.succ_lt_succ_iff.mp h), + ih (Nat.le_of_succ_le h)]; rfl + +@[simp] theorem dfoldr_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.succ → α i.castSucc) + (x : α 0) : dfoldr 0 α f x = x := + dfoldr_loop_zero .. + +theorem dfoldr_succ {n : Nat} {α : Fin (n+2) → Sort _} + (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : + dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := + dfoldr_loop .. + +theorem dfoldr_succ_last {n : Nat} {α : Fin (n+2) → Sort _} + (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : + dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by + induction n with + | zero => simp only [dfoldr_succ, dfoldr_zero, last, zero_eta] + | succ n ih => rw [dfoldr_succ, ih (α := α ∘ succ) (f ·.succ), dfoldr_succ]; congr + +theorem dfoldr_eq_dfoldrM {n : Nat} {α : Fin (n+1) → Type _} + (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α (last n)) : + dfoldr n α f x = dfoldrM (m:=Id) n α f x := by + induction n <;> simp [dfoldr_succ, dfoldrM_succ, *] + +/-- Dependent version `dfoldr` equals non-dependent version `foldr` -/ +theorem dfoldr_eq_foldr {n : Nat} {α : Sort _} (f : Fin n → α → α) (x : α) : + dfoldr n (fun _ => α) f x = foldr n f x := by + induction n with + | zero => simp only [dfoldr_zero, foldr_zero] + | succ n ih => simp only [dfoldr_succ, foldr_succ, Function.comp_apply, Function.comp_def, ih] + +-- TODO: add `dfoldl_rev` and `dfoldr_rev` + +/-! ### `Fin.fold{l/r}{M}` equals `List.fold{l/r}{M}` -/ + theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x) : foldlM n f x = (List.finRange n).foldlM f x := by induction n generalizing x with diff --git a/Batteries/Data/Fin/Lemmas.lean b/Batteries/Data/Fin/Lemmas.lean index 90de53225b..ddc7bbf1cf 100644 --- a/Batteries/Data/Fin/Lemmas.lean +++ b/Batteries/Data/Fin/Lemmas.lean @@ -13,96 +13,3 @@ attribute [norm_cast] val_last /-! ### clamp -/ @[simp] theorem coe_clamp (n m : Nat) : (clamp n m : Nat) = min n m := rfl - -/-! ### foldM -/ - -variable {n : Nat} {α : Fin (n+1) → Type _} [Monad m] - (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) - -theorem foldM_loop_lt (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - foldM.loop n α f i (Nat.lt_add_right 1 h) x = - (f ⟨i, h⟩ x) >>= (foldM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by - rw [foldM.loop, dif_pos h] - -theorem foldM_loop_eq (x : α ⟨n, Nat.le_refl _⟩) : - foldM.loop n α f n (Nat.le_refl _) x = pure x := by - rw [foldM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] - -@[simp] theorem foldM_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) - (x : α 0) : foldM 0 α f x = pure x := - foldM_loop_eq .. - -variable {α : Fin (n+2) → Type _} (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) - -theorem foldM_loop (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - foldM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = - f ⟨i, h⟩ x >>= (foldM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by - if h' : i < n then - rw [foldM_loop_lt _ h _] - congr; funext - rw [foldM_loop_lt _ h' _, foldM_loop]; rfl - else - cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') - rw [foldM_loop_lt] - congr; funext - rw [foldM_loop_eq, foldM_loop_eq] - -theorem foldM_succ (x) : foldM (n+1) α f x = f 0 x >>= foldM n (α ∘ succ) (f ·.succ ·) := - foldM_loop .. - -/-- Dependent version `foldM` equals non-dependent version `foldlM` --/ -theorem foldM_eq_foldlM {α : Type _} (f : Fin n → α → m α) (x : α) : - foldM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by - induction n generalizing x with - | zero => simp only [foldM_zero, foldlM_zero] - | succ n ih => - simp only [foldM_succ, foldlM_succ, Function.comp_apply, Function.comp_def] - congr; ext; simp only [ih] - -/-! ### fold -/ - -variable {α : Fin (n+1) → Sort _} (f : ∀ (i : Fin n), α i.castSucc → α i.succ) - -theorem fold_loop_lt (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - fold.loop n α f i (Nat.lt_add_right 1 h) x = - fold.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by - rw [fold.loop, dif_pos h] - -theorem fold_loop_eq (x : α ⟨n, Nat.le_refl _⟩) : - fold.loop n α f n (Nat.le_refl _) x = x := by - rw [fold.loop, dif_neg (Nat.lt_irrefl _), cast_eq] - -@[simp] theorem fold_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.castSucc → α i.succ) - (x : α 0) : fold 0 α f x = x := - fold_loop_eq .. - -variable {α : Fin (n+2) → Sort _} (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) - -theorem fold_loop (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - fold.loop (n+1) α f i (Nat.lt_add_right 1 h) x = - fold.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by - if h' : i < n then - rw [fold_loop_lt _ h _] - rw [fold_loop_lt _ h' _, fold_loop]; rfl - else - cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') - rw [fold_loop_lt] - rw [fold_loop_eq, fold_loop_eq] - -theorem fold_succ (x : α 0) : fold (n+1) α f x = fold n (α ∘ succ) (f ·.succ ·) (f 0 x) := - fold_loop .. - -theorem fold_succ_last (x : α 0) : - fold (n+1) α f x = f (last n) (fold n (α ∘ castSucc) (f ·.castSucc ·) x) := by - rw [fold_succ] - induction n with - | zero => simp [fold_succ, last] - | succ n ih => rw [fold_succ, @ih (α ∘ succ) (f ·.succ ·), fold_succ]; congr - -theorem fold_eq_foldl {α : Sort _} (f : Fin n → α → α) (x : α) : - fold n (fun _ => α) f x = foldl n (fun x i => f i x) x := by - induction n generalizing x with - | zero => simp only [fold_zero, foldl_zero] - | succ n ih => - simp only [fold_succ, foldl_succ, Function.comp_apply, Function.comp_def] - congr; simp only [ih] From a67ab9c499064635634963dfc7ac51008c63de40 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Mon, 2 Dec 2024 15:45:46 -0700 Subject: [PATCH 07/14] changed attributes according to suggestion --- Batteries/Data/Fin/Basic.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 2f3be2db65..28908a22fe 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -19,7 +19,7 @@ alias enum := Array.finRange alias list := List.finRange /-- Dependent version of `Fin.foldlM`. -/ -@[specialize] def dfoldlM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) +@[inline] def dfoldlM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n)) := loop 0 (Nat.zero_lt_succ n) init where /-- Inner loop for `Fin.dfoldlM`. @@ -39,7 +39,7 @@ alias list := List.finRange _root_.cast (congrArg (fun i => m (α i)) this) (pure x) /-- Dependent version of `Fin.foldrM`. -/ -@[specialize] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) +@[inline] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0) := loop n (Nat.lt_succ_self n) init where /-- Inner loop for `Fin.foldRevM`. @@ -61,11 +61,11 @@ alias list := List.finRange _root_.cast (congrArg (fun i => m (α i)) this) (pure x) /-- Dependent version of `Fin.foldl`. -/ -@[specialize] def dfoldl (n : Nat) (α : Fin (n + 1) → Sort _) +@[inline] def dfoldl (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := loop 0 (Nat.zero_lt_succ n) init where /-- Inner loop for `Fin.dfoldl`. `Fin.dfoldl.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/ - loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α (last n) := + @[semireducible] 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 @@ -73,7 +73,7 @@ alias list := List.finRange _root_.cast (congrArg α this) x /-- Dependent version of `Fin.foldr`. -/ -@[specialize] def dfoldr (n : Nat) (α : Fin (n + 1) → Sort _) +@[inline] def dfoldr (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := loop n (Nat.lt_succ_self n) init where /-- Inner loop for `Fin.dfoldr`. From 84b4d68d600394e4bca624813609904f0324f45b Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Mon, 2 Dec 2024 15:51:47 -0700 Subject: [PATCH 08/14] added `semireducible` attribute to all inner loops --- Batteries/Data/Fin/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 28908a22fe..98afb372d2 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -31,7 +31,7 @@ alias list := List.finRange pure xₙ ``` -/ - loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α (last n)) := + @[semireducible] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α (last n)) := if h' : i < n then (f ⟨i, h'⟩ x) >>= loop (i + 1) (Nat.succ_lt_succ h') else @@ -52,7 +52,7 @@ alias list := List.finRange pure x₀ ``` -/ - loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α 0) := + @[semireducible] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α 0) := if h' : i > 0 then (f ⟨i - 1, by omega⟩ (by simpa [Nat.sub_one_add_one_eq_of_pos h'] using x)) >>= loop (i - 1) (by omega) @@ -78,7 +78,7 @@ alias list := List.finRange loop n (Nat.lt_succ_self n) init where /-- Inner loop for `Fin.dfoldr`. `Fin.dfoldr.loop n α f i h x = f 0 (f 1 (... (f i x)))` -/ - loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := + @[semireducible] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := if h' : i > 0 then loop (i - 1) (by omega) (f ⟨i - 1, by omega⟩ (by simpa [Nat.sub_one_add_one_eq_of_pos h'] using x)) From 5339692f488c39af081210ae5e2668ee4fdafc52 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Mon, 2 Dec 2024 17:03:29 -0700 Subject: [PATCH 09/14] fixed error --- Batteries/Data/Fin/Fold.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index 8bcb1d644a..a7923ca34f 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -80,7 +80,7 @@ theorem dfoldrM_loop [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Typ | zero => rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind] conv => rhs; rw [←bind_pure (f 0 x)] - congr; funext; exact dfoldrM_loop_zero .. + congr | succ i ih => rw [dfoldrM_loop_succ _ h, dfoldrM_loop_succ _ (Nat.succ_lt_succ_iff.mp h), bind_assoc] congr; funext; exact ih .. From 5c0e5befa438aa8d9698da560999932b4f373ecf Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 2 Dec 2024 21:33:15 -0500 Subject: [PATCH 10/14] fix: use auto-implicit --- Batteries/Data/Fin/Fold.lean | 64 ++++++++++++++++-------------------- 1 file changed, 28 insertions(+), 36 deletions(-) diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index a7923ca34f..7514f13690 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -1,7 +1,7 @@ /- 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 +Authors: François G. Dorais, Quang Dao -/ import Batteries.Data.List.FinRange import Batteries.Data.Fin.Basic @@ -10,24 +10,24 @@ namespace Fin /-! ### dfoldlM -/ -theorem dfoldlM_loop_lt [Monad m] {n : Nat} {α : Fin (n+1) → Type _} +theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x = (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by rw [dfoldlM.loop, dif_pos h] -theorem dfoldlM_loop_eq [Monad m] {n : Nat} {α : Fin (n+1) → Type _} +theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x : α ⟨n, Nat.le_refl _⟩) : dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -@[simp] theorem dfoldlM_zero [Monad m] {α : Fin 1 → Type _} +@[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x : α 0) : dfoldlM 0 α f x = pure x := dfoldlM_loop_eq .. -theorem dfoldlM_loop [Monad m] {n : Nat} {α : Fin (n+2) → Type _} +theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = @@ -42,13 +42,12 @@ theorem dfoldlM_loop [Monad m] {n : Nat} {α : Fin (n+2) → Type _} congr; funext rw [dfoldlM_loop_eq, dfoldlM_loop_eq] -theorem dfoldlM_succ [Monad m] {n : Nat} {α : Fin (n+2) → Type _} +theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x : α 0) : dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) := dfoldlM_loop .. -/-- Dependent version `dfoldlM` equals non-dependent version `foldlM` -/ -theorem dfoldlM_eq_foldlM [Monad m] {n : Nat} {α : Type _} (f : (i : Fin n) → α → m α) (x : α) : +theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) : dfoldlM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by induction n generalizing x with | zero => simp only [dfoldlM_zero, foldlM_zero] @@ -58,12 +57,12 @@ theorem dfoldlM_eq_foldlM [Monad m] {n : Nat} {α : Type _} (f : (i : Fin n) → /-! ### dfoldrM -/ -theorem dfoldrM_loop_zero [Monad m] {n : Nat} {α : Fin (n+1) → Type _} +theorem dfoldrM_loop_zero [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α 0) : dfoldrM.loop n α f 0 (Nat.zero_lt_succ n) x = pure x := by rw [dfoldrM.loop, dif_neg (Nat.not_lt_zero _), cast_eq] -theorem dfoldrM_loop_succ [Monad m] {n : Nat} {α : Fin (n+1) → Type _} +theorem dfoldrM_loop_succ [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (h : i < n) (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : dfoldrM.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = @@ -71,7 +70,7 @@ theorem dfoldrM_loop_succ [Monad m] {n : Nat} {α : Fin (n+1) → Type _} rw [dfoldrM.loop, dif_pos (Nat.zero_lt_succ i)] simp only [Nat.add_one_sub_one, castSucc_mk, succ_mk, eq_mpr_eq_cast, cast_eq] -theorem dfoldrM_loop [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Type _} +theorem dfoldrM_loop [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) (h : i+1 ≤ n+1) (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : dfoldrM.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = @@ -85,18 +84,17 @@ theorem dfoldrM_loop [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Typ rw [dfoldrM_loop_succ _ h, dfoldrM_loop_succ _ (Nat.succ_lt_succ_iff.mp h), bind_assoc] congr; funext; exact ih .. -@[simp] theorem dfoldrM_zero [Monad m] {α : Fin 1 → Type _} +@[simp] theorem dfoldrM_zero [Monad m] (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x : α 0) : dfoldrM 0 α f x = pure x := dfoldrM_loop_zero .. -theorem dfoldrM_succ [Monad m] [LawfulMonad m] {n : Nat} {α : Fin (n+2) → Type _} +theorem dfoldrM_succ [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) (x : α (last (n+1))) : dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := dfoldrM_loop .. -/-- Dependent version `dfoldrM` equals non-dependent version `foldrM` -/ -theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] {n : Nat} {α : Type _} +theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] (f : (i : Fin n) → α → m α) (x : α) : dfoldrM n (fun _ => α) f x = foldrM n f x := by induction n generalizing x with | zero => simp only [dfoldrM_zero, foldrM_zero] @@ -104,23 +102,20 @@ theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] {n : Nat} {α : Type _} /-! ### dfoldl -/ -theorem dfoldl_loop_lt {n : Nat} {α : Fin (n+1) → Sort _} - (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : +theorem dfoldl_loop_lt (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : dfoldl.loop n α f i (Nat.lt_add_right 1 h) x = dfoldl.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by rw [dfoldl.loop, dif_pos h] -theorem dfoldl_loop_eq {n : Nat} {α : Fin (n+1) → Sort _} - (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x : α ⟨n, Nat.le_refl _⟩) : +theorem dfoldl_loop_eq (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x : α ⟨n, Nat.le_refl _⟩) : dfoldl.loop n α f n (Nat.le_refl _) x = x := by rw [dfoldl.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -@[simp] theorem dfoldl_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.castSucc → α i.succ) +@[simp] theorem dfoldl_zero (f : (i : Fin 0) → α i.castSucc → α i.succ) (x : α 0) : dfoldl 0 α f x = x := dfoldl_loop_eq .. -theorem dfoldl_loop {n : Nat} {α : Fin (n+2) → Sort _} - (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) +theorem dfoldl_loop (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : dfoldl.loop (n+1) α f i (Nat.lt_add_right 1 h) x = dfoldl.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by @@ -132,12 +127,11 @@ theorem dfoldl_loop {n : Nat} {α : Fin (n+2) → Sort _} rw [dfoldl_loop_lt] rw [dfoldl_loop_eq, dfoldl_loop_eq] -theorem dfoldl_succ {n : Nat} {α : Fin (n+2) → Sort _} - (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : +theorem dfoldl_succ (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : dfoldl (n+1) α f x = dfoldl n (α ∘ succ) (f ·.succ ·) (f 0 x) := dfoldl_loop .. -theorem dfoldl_succ_last {n : Nat} {α : Fin (n+2) → Sort _} +theorem dfoldl_succ_last (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x) := by rw [dfoldl_succ] @@ -145,8 +139,7 @@ theorem dfoldl_succ_last {n : Nat} {α : Fin (n+2) → Sort _} | zero => simp [dfoldl_succ, last] | succ n ih => rw [dfoldl_succ, @ih (α ∘ succ) (f ·.succ ·), dfoldl_succ]; congr -/-- Dependent version `dfoldl` equals non-dependent version `foldl` -/ -theorem dfoldl_eq_foldl {α : Sort _} (f : Fin n → α → α) (x : α) : +theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) : dfoldl n (fun _ => α) f x = foldl n (fun x i => f i x) x := by induction n generalizing x with | zero => simp only [dfoldl_zero, foldl_zero] @@ -156,12 +149,12 @@ theorem dfoldl_eq_foldl {α : Sort _} (f : Fin n → α → α) (x : α) : /-! ### dfoldr -/ -theorem dfoldr_loop_zero {n : Nat} {α : Fin (n+1) → Sort _} +theorem dfoldr_loop_zero (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α 0) : dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := by rw [dfoldr.loop, dif_neg (Nat.not_lt_zero _), cast_eq] -theorem dfoldr_loop_succ {n : Nat} {α : Fin (n+1) → Sort _} +theorem dfoldr_loop_succ (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = @@ -169,7 +162,7 @@ theorem dfoldr_loop_succ {n : Nat} {α : Fin (n+1) → Sort _} rw [dfoldr.loop, dif_pos (Nat.zero_lt_succ i)] simp only [Nat.add_one_sub_one, succ_mk, eq_mpr_eq_cast, cast_eq] -theorem dfoldr_loop {n : Nat} {α : Fin (n+2) → Sort _} +theorem dfoldr_loop (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = @@ -179,29 +172,28 @@ theorem dfoldr_loop {n : Nat} {α : Fin (n+2) → Sort _} | succ i ih => rw [dfoldr_loop_succ _ h, dfoldr_loop_succ _ (Nat.succ_lt_succ_iff.mp h), ih (Nat.le_of_succ_le h)]; rfl -@[simp] theorem dfoldr_zero {α : Fin 1 → Sort _} (f : (i : Fin 0) → α i.succ → α i.castSucc) +@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) (x : α 0) : dfoldr 0 α f x = x := dfoldr_loop_zero .. -theorem dfoldr_succ {n : Nat} {α : Fin (n+2) → Sort _} +theorem dfoldr_succ (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := dfoldr_loop .. -theorem dfoldr_succ_last {n : Nat} {α : Fin (n+2) → Sort _} +theorem dfoldr_succ_last (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by induction n with | zero => simp only [dfoldr_succ, dfoldr_zero, last, zero_eta] | succ n ih => rw [dfoldr_succ, ih (α := α ∘ succ) (f ·.succ), dfoldr_succ]; congr -theorem dfoldr_eq_dfoldrM {n : Nat} {α : Fin (n+1) → Type _} +theorem dfoldr_eq_dfoldrM (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α (last n)) : dfoldr n α f x = dfoldrM (m:=Id) n α f x := by induction n <;> simp [dfoldr_succ, dfoldrM_succ, *] -/-- Dependent version `dfoldr` equals non-dependent version `foldr` -/ -theorem dfoldr_eq_foldr {n : Nat} {α : Sort _} (f : Fin n → α → α) (x : α) : +theorem dfoldr_eq_foldr (f : Fin n → α → α) (x : α) : dfoldr n (fun _ => α) f x = foldr n f x := by induction n with | zero => simp only [dfoldr_zero, foldr_zero] From be0ea0f17ffec9da67511d12dde958c1ed425164 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 3 Dec 2024 13:16:56 -0500 Subject: [PATCH 11/14] fix: style --- Batteries/Data/Fin/Fold.lean | 138 ++++++++++++++--------------------- 1 file changed, 53 insertions(+), 85 deletions(-) diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index 7514f13690..513e5f6cf3 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -10,28 +10,21 @@ namespace Fin /-! ### dfoldlM -/ -theorem dfoldlM_loop_lt [Monad m] - (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) - (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x = - (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by +theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x) : + dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x = + (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by rw [dfoldlM.loop, dif_pos h] -theorem dfoldlM_loop_eq [Monad m] - (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x : α ⟨n, Nat.le_refl _⟩) : - dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by +theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) : + dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -@[simp] theorem dfoldlM_zero [Monad m] - (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x : α 0) : - dfoldlM 0 α f x = pure x := - dfoldlM_loop_eq .. +@[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) : + dfoldlM 0 α f x = pure x := dfoldlM_loop_eq .. -theorem dfoldlM_loop [Monad m] - (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) - (h : i < n+1) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = - f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by +theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1) + (x) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by if h' : i < n then rw [dfoldlM_loop_lt _ h _] congr; funext @@ -42,9 +35,8 @@ theorem dfoldlM_loop [Monad m] congr; funext rw [dfoldlM_loop_eq, dfoldlM_loop_eq] -theorem dfoldlM_succ [Monad m] - (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x : α 0) : - dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) := +theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x) : + dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) := dfoldlM_loop .. theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) : @@ -57,24 +49,19 @@ theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) : /-! ### dfoldrM -/ -theorem dfoldrM_loop_zero [Monad m] - (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α 0) : - dfoldrM.loop n α f 0 (Nat.zero_lt_succ n) x = pure x := by +theorem dfoldrM_loop_zero [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x) : + dfoldrM.loop n α f 0 (Nat.zero_lt_succ n) x = pure x := by rw [dfoldrM.loop, dif_neg (Nat.not_lt_zero _), cast_eq] -theorem dfoldrM_loop_succ [Monad m] - (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (h : i < n) - (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : - dfoldrM.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = - f ⟨i, h⟩ x >>= dfoldrM.loop n α f i (Nat.lt_add_right 1 h) := by +theorem dfoldrM_loop_succ [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (h : i < n) + (x) : dfoldrM.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = + f ⟨i, h⟩ x >>= dfoldrM.loop n α f i (Nat.lt_add_right 1 h) := by rw [dfoldrM.loop, dif_pos (Nat.zero_lt_succ i)] simp only [Nat.add_one_sub_one, castSucc_mk, succ_mk, eq_mpr_eq_cast, cast_eq] -theorem dfoldrM_loop [Monad m] [LawfulMonad m] - (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) (h : i+1 ≤ n+1) - (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : - dfoldrM.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = - dfoldrM.loop n (α ∘ succ) (f ·.succ) i h x >>= f 0 := by +theorem dfoldrM_loop [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) + (h : i+1 ≤ n+1) (x) : dfoldrM.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = + dfoldrM.loop n (α ∘ succ) (f ·.succ) i h x >>= f 0 := by induction i with | zero => rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind] @@ -84,41 +71,35 @@ theorem dfoldrM_loop [Monad m] [LawfulMonad m] rw [dfoldrM_loop_succ _ h, dfoldrM_loop_succ _ (Nat.succ_lt_succ_iff.mp h), bind_assoc] congr; funext; exact ih .. -@[simp] theorem dfoldrM_zero [Monad m] - (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x : α 0) : - dfoldrM 0 α f x = pure x := - dfoldrM_loop_zero .. +@[simp] theorem dfoldrM_zero [Monad m] (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x) : + dfoldrM 0 α f x = pure x := dfoldrM_loop_zero .. -theorem dfoldrM_succ [Monad m] [LawfulMonad m] - (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) (x : α (last (n+1))) : - dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := - dfoldrM_loop .. +theorem dfoldrM_succ [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) + (x) : dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := dfoldrM_loop .. -theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] - (f : (i : Fin n) → α → m α) (x : α) : dfoldrM n (fun _ => α) f x = foldrM n f x := by +theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] (f : (i : Fin n) → α → m α) (x : α) : + dfoldrM n (fun _ => α) f x = foldrM n f x := by induction n generalizing x with | zero => simp only [dfoldrM_zero, foldrM_zero] | succ n ih => simp only [dfoldrM_succ, foldrM_succ, Function.comp_def, ih] /-! ### dfoldl -/ -theorem dfoldl_loop_lt (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - dfoldl.loop n α f i (Nat.lt_add_right 1 h) x = - dfoldl.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by +theorem dfoldl_loop_lt (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (h : i < n) (x) : + dfoldl.loop n α f i (Nat.lt_add_right 1 h) x = + dfoldl.loop n α f (i+1) (Nat.add_lt_add_right h 1) (f ⟨i, h⟩ x) := by rw [dfoldl.loop, dif_pos h] -theorem dfoldl_loop_eq (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x : α ⟨n, Nat.le_refl _⟩) : - dfoldl.loop n α f n (Nat.le_refl _) x = x := by +theorem dfoldl_loop_eq (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (x) : + dfoldl.loop n α f n (Nat.le_refl _) x = x := by rw [dfoldl.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -@[simp] theorem dfoldl_zero (f : (i : Fin 0) → α i.castSucc → α i.succ) - (x : α 0) : dfoldl 0 α f x = x := - dfoldl_loop_eq .. +@[simp] theorem dfoldl_zero (f : (i : Fin 0) → α i.castSucc → α i.succ) (x) : + dfoldl 0 α f x = x := dfoldl_loop_eq .. -theorem dfoldl_loop (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) - (x : α ⟨i, Nat.lt_add_right 1 h⟩) : - dfoldl.loop (n+1) α f i (Nat.lt_add_right 1 h) x = - dfoldl.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by +theorem dfoldl_loop (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i < n+1) (x) : + dfoldl.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + dfoldl.loop n (α ∘ succ) (f ·.succ ·) i h (f ⟨i, h⟩ x) := by if h' : i < n then rw [dfoldl_loop_lt _ h _] rw [dfoldl_loop_lt _ h' _, dfoldl_loop]; rfl @@ -127,13 +108,11 @@ theorem dfoldl_loop (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (h : i rw [dfoldl_loop_lt] rw [dfoldl_loop_eq, dfoldl_loop_eq] -theorem dfoldl_succ (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : - dfoldl (n+1) α f x = dfoldl n (α ∘ succ) (f ·.succ ·) (f 0 x) := - dfoldl_loop .. +theorem dfoldl_succ (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) : + dfoldl (n+1) α f x = dfoldl n (α ∘ succ) (f ·.succ ·) (f 0 x) := dfoldl_loop .. -theorem dfoldl_succ_last - (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x : α 0) : - dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x) := by +theorem dfoldl_succ_last (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) : + dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x) := by rw [dfoldl_succ] induction n with | zero => simp [dfoldl_succ, last] @@ -149,22 +128,17 @@ theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) : /-! ### dfoldr -/ -theorem dfoldr_loop_zero - (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α 0) : - dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := by +theorem dfoldr_loop_zero (f : (i : Fin n) → α i.succ → α i.castSucc) (x) : + dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := by rw [dfoldr.loop, dif_neg (Nat.not_lt_zero _), cast_eq] -theorem dfoldr_loop_succ - (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) - (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : +theorem dfoldr_loop_succ (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) (x) : dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = dfoldr.loop n α f i (Nat.lt_add_right 1 h) (f ⟨i, h⟩ x) := by rw [dfoldr.loop, dif_pos (Nat.zero_lt_succ i)] simp only [Nat.add_one_sub_one, succ_mk, eq_mpr_eq_cast, cast_eq] -theorem dfoldr_loop - (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) - (x : α ⟨i+1, Nat.add_lt_add_right h 1⟩) : +theorem dfoldr_loop (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) (x) : dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = f 0 (dfoldr.loop n (α ∘ succ) (f ·.succ) i h x) := by induction i with @@ -172,29 +146,23 @@ theorem dfoldr_loop | succ i ih => rw [dfoldr_loop_succ _ h, dfoldr_loop_succ _ (Nat.succ_lt_succ_iff.mp h), ih (Nat.le_of_succ_le h)]; rfl -@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) - (x : α 0) : dfoldr 0 α f x = x := - dfoldr_loop_zero .. +@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) (x) : + dfoldr 0 α f x = x := dfoldr_loop_zero .. -theorem dfoldr_succ - (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : - dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := - dfoldr_loop .. +theorem dfoldr_succ (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) : + dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := dfoldr_loop .. -theorem dfoldr_succ_last - (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x : α (last (n+1))) : - dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by +theorem dfoldr_succ_last (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) : + dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by induction n with | zero => simp only [dfoldr_succ, dfoldr_zero, last, zero_eta] | succ n ih => rw [dfoldr_succ, ih (α := α ∘ succ) (f ·.succ), dfoldr_succ]; congr -theorem dfoldr_eq_dfoldrM - (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α (last n)) : - dfoldr n α f x = dfoldrM (m:=Id) n α f x := by +theorem dfoldr_eq_dfoldrM (f : (i : Fin n) → α i.succ → α i.castSucc) (x) : + dfoldr n α f x = dfoldrM (m:=Id) n α f x := by induction n <;> simp [dfoldr_succ, dfoldrM_succ, *] -theorem dfoldr_eq_foldr (f : Fin n → α → α) (x : α) : - dfoldr n (fun _ => α) f x = foldr n f x := by +theorem dfoldr_eq_foldr (f : Fin n → α → α) (x : α) : dfoldr n (fun _ => α) f x = foldr n f x := by induction n with | zero => simp only [dfoldr_zero, foldr_zero] | succ n ih => simp only [dfoldr_succ, foldr_succ, Function.comp_apply, Function.comp_def, ih] From 995fa6ee27809d54ebb87a5402895f9a03ef77e4 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Tue, 3 Dec 2024 18:35:31 -0600 Subject: [PATCH 12/14] made suggested changes (except redefining monadic version) --- Batteries/Data/Fin/Basic.lean | 13 +++++-------- Batteries/Data/Fin/Fold.lean | 5 ++--- 2 files changed, 7 insertions(+), 11 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 98afb372d2..7323f70eee 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -65,7 +65,7 @@ alias list := List.finRange (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := loop 0 (Nat.zero_lt_succ n) init where /-- Inner loop for `Fin.dfoldl`. `Fin.dfoldl.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/ - @[semireducible] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α (last n) := + @[semireducible, specialize] 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 @@ -78,10 +78,7 @@ alias list := List.finRange loop n (Nat.lt_succ_self n) init where /-- Inner loop for `Fin.dfoldr`. `Fin.dfoldr.loop n α f i h x = f 0 (f 1 (... (f i x)))` -/ - @[semireducible] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := - if h' : i > 0 then - loop (i - 1) (by omega) (f ⟨i - 1, by omega⟩ - (by simpa [Nat.sub_one_add_one_eq_of_pos h'] using x)) - else - haveI : ⟨i, h⟩ = 0 := by ext; simp; omega - _root_.cast (congrArg α this) x + @[specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := + match i with + | i + 1 => loop i (Nat.lt_of_succ_lt h) (f ⟨i, Nat.lt_of_succ_lt_succ h⟩ x) + | 0 => x diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index 513e5f6cf3..6c2842e224 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -130,13 +130,12 @@ theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) : theorem dfoldr_loop_zero (f : (i : Fin n) → α i.succ → α i.castSucc) (x) : dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := by - rw [dfoldr.loop, dif_neg (Nat.not_lt_zero _), cast_eq] + rw [dfoldr.loop] theorem dfoldr_loop_succ (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) (x) : dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = dfoldr.loop n α f i (Nat.lt_add_right 1 h) (f ⟨i, h⟩ x) := by - rw [dfoldr.loop, dif_pos (Nat.zero_lt_succ i)] - simp only [Nat.add_one_sub_one, succ_mk, eq_mpr_eq_cast, cast_eq] + rw [dfoldr.loop] theorem dfoldr_loop (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) (x) : dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = From 62ba9ac0cbcd3bc58c278b4deb5467c774bd358a Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 3 Dec 2024 20:41:32 -0500 Subject: [PATCH 13/14] refactor: simplify `dfoldrM` --- Batteries/Data/Fin/Basic.lean | 75 +++++++---------- Batteries/Data/Fin/Fold.lean | 154 ++++++++++++++-------------------- 2 files changed, 92 insertions(+), 137 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index 7323f70eee..ef5a1f57f0 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -18,6 +18,34 @@ alias enum := Array.finRange @[deprecated (since := "2024-11-15")] alias list := List.finRange +/-- Dependent version of `Fin.foldr`. -/ +@[inline] def dfoldr (n : Nat) (α : Fin (n + 1) → Sort _) + (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := + loop n (Nat.lt_succ_self n) init where + /-- Inner loop for `Fin.dfoldr`. + `Fin.dfoldr.loop n α f i h x = f 0 (f 1 (... (f i x)))` -/ + @[specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := + match i with + | i + 1 => loop i (Nat.lt_of_succ_lt h) (f ⟨i, Nat.lt_of_succ_lt_succ h⟩ x) + | 0 => x + +/-- Dependent version of `Fin.foldrM`. -/ +@[inline] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) + (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0) := + dfoldr n (fun i => m (α i)) (fun i x => x >>= f i) (pure init) + +/-- Dependent version of `Fin.foldl`. -/ +@[inline] def dfoldl (n : Nat) (α : Fin (n + 1) → Sort _) + (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := + loop 0 (Nat.zero_lt_succ n) init where + /-- Inner loop for `Fin.dfoldl`. `Fin.dfoldl.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/ + @[semireducible, specialize] 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; omega + _root_.cast (congrArg α this) x + /-- Dependent version of `Fin.foldlM`. -/ @[inline] def dfoldlM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n)) := @@ -31,54 +59,9 @@ alias list := List.finRange pure xₙ ``` -/ - @[semireducible] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α (last n)) := + @[semireducible, specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α (last n)) := if h' : i < n then (f ⟨i, h'⟩ x) >>= loop (i + 1) (Nat.succ_lt_succ h') else haveI : ⟨i, h⟩ = last n := by ext; simp; omega _root_.cast (congrArg (fun i => m (α i)) this) (pure x) - -/-- Dependent version of `Fin.foldrM`. -/ -@[inline] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) - (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0) := - loop n (Nat.lt_succ_self n) init where - /-- Inner loop for `Fin.foldRevM`. - ``` - Fin.foldRevM.loop n α f i h xᵢ = do - let xᵢ₋₁ ← f (i+1) xᵢ - ... - let x₁ ← f 1 x₂ - let x₀ ← f 0 x₁ - pure x₀ - ``` - -/ - @[semireducible] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : m (α 0) := - if h' : i > 0 then - (f ⟨i - 1, by omega⟩ (by simpa [Nat.sub_one_add_one_eq_of_pos h'] using x)) - >>= loop (i - 1) (by omega) - else - haveI : ⟨i, h⟩ = 0 := by ext; simp; omega - _root_.cast (congrArg (fun i => m (α i)) this) (pure x) - -/-- Dependent version of `Fin.foldl`. -/ -@[inline] def dfoldl (n : Nat) (α : Fin (n + 1) → Sort _) - (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := - loop 0 (Nat.zero_lt_succ n) init where - /-- Inner loop for `Fin.dfoldl`. `Fin.dfoldl.loop n α f i h x = f n (f (n-1) (... (f i x)))` -/ - @[semireducible, specialize] 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; omega - _root_.cast (congrArg α this) x - -/-- Dependent version of `Fin.foldr`. -/ -@[inline] def dfoldr (n : Nat) (α : Fin (n + 1) → Sort _) - (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := - loop n (Nat.lt_succ_self n) init where - /-- Inner loop for `Fin.dfoldr`. - `Fin.dfoldr.loop n α f i h x = f 0 (f 1 (... (f i x)))` -/ - @[specialize] loop (i : Nat) (h : i < n + 1) (x : α ⟨i, h⟩) : α 0 := - match i with - | i + 1 => loop i (Nat.lt_of_succ_lt h) (f ⟨i, Nat.lt_of_succ_lt_succ h⟩ x) - | 0 => x diff --git a/Batteries/Data/Fin/Fold.lean b/Batteries/Data/Fin/Fold.lean index 6c2842e224..51d2f0c53c 100644 --- a/Batteries/Data/Fin/Fold.lean +++ b/Batteries/Data/Fin/Fold.lean @@ -8,74 +8,49 @@ import Batteries.Data.Fin.Basic namespace Fin -/-! ### dfoldlM -/ - -theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x) : - dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x = - (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by - rw [dfoldlM.loop, dif_pos h] +/-! ### dfoldr -/ -theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) : - dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by - rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] +theorem dfoldr_loop_zero (f : (i : Fin n) → α i.succ → α i.castSucc) (x) : + dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := rfl -@[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) : - dfoldlM 0 α f x = pure x := dfoldlM_loop_eq .. +theorem dfoldr_loop_succ (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) (x) : + dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = + dfoldr.loop n α f i (Nat.lt_add_right 1 h) (f ⟨i, h⟩ x) := rfl -theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1) - (x) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = - f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by - if h' : i < n then - rw [dfoldlM_loop_lt _ h _] - congr; funext - rw [dfoldlM_loop_lt _ h' _, dfoldlM_loop]; rfl - else - cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') - rw [dfoldlM_loop_lt] - congr; funext - rw [dfoldlM_loop_eq, dfoldlM_loop_eq] +theorem dfoldr_loop (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) (x) : + dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = + f 0 (dfoldr.loop n (α ∘ succ) (f ·.succ) i h x) := by + induction i with + | zero => rfl + | succ i ih => exact ih .. -theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x) : - dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) := - dfoldlM_loop .. +@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) (x) : + dfoldr 0 α f x = x := rfl -theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) : - dfoldlM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by - induction n generalizing x with - | zero => simp only [dfoldlM_zero, foldlM_zero] - | succ n ih => - simp only [dfoldlM_succ, foldlM_succ, Function.comp_apply, Function.comp_def] - congr; ext; simp only [ih] +theorem dfoldr_succ (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) : + dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := dfoldr_loop .. -/-! ### dfoldrM -/ +theorem dfoldr_succ_last (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) : + dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by + induction n with + | zero => simp only [dfoldr_succ, dfoldr_zero, last, zero_eta] + | succ n ih => rw [dfoldr_succ, ih (α := α ∘ succ) (f ·.succ), dfoldr_succ]; congr -theorem dfoldrM_loop_zero [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x) : - dfoldrM.loop n α f 0 (Nat.zero_lt_succ n) x = pure x := by - rw [dfoldrM.loop, dif_neg (Nat.not_lt_zero _), cast_eq] +theorem dfoldr_eq_dfoldrM (f : (i : Fin n) → α i.succ → α i.castSucc) (x) : + dfoldr n α f x = dfoldrM (m:=Id) n α f x := rfl -theorem dfoldrM_loop_succ [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (h : i < n) - (x) : dfoldrM.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = - f ⟨i, h⟩ x >>= dfoldrM.loop n α f i (Nat.lt_add_right 1 h) := by - rw [dfoldrM.loop, dif_pos (Nat.zero_lt_succ i)] - simp only [Nat.add_one_sub_one, castSucc_mk, succ_mk, eq_mpr_eq_cast, cast_eq] +theorem dfoldr_eq_foldr (f : Fin n → α → α) (x : α) : dfoldr n (fun _ => α) f x = foldr n f x := by + induction n with + | zero => simp only [dfoldr_zero, foldr_zero] + | succ n ih => simp only [dfoldr_succ, foldr_succ, Function.comp_apply, Function.comp_def, ih] -theorem dfoldrM_loop [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) - (h : i+1 ≤ n+1) (x) : dfoldrM.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = - dfoldrM.loop n (α ∘ succ) (f ·.succ) i h x >>= f 0 := by - induction i with - | zero => - rw [dfoldrM_loop_zero, dfoldrM_loop_succ, pure_bind] - conv => rhs; rw [←bind_pure (f 0 x)] - congr - | succ i ih => - rw [dfoldrM_loop_succ _ h, dfoldrM_loop_succ _ (Nat.succ_lt_succ_iff.mp h), bind_assoc] - congr; funext; exact ih .. +/-! ### dfoldrM -/ @[simp] theorem dfoldrM_zero [Monad m] (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x) : - dfoldrM 0 α f x = pure x := dfoldrM_loop_zero .. + dfoldrM 0 α f x = pure x := rfl -theorem dfoldrM_succ [Monad m] [LawfulMonad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) - (x) : dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := dfoldrM_loop .. +theorem dfoldrM_succ [Monad m] (f : (i : Fin (n+1)) → α i.succ → m (α i.castSucc)) + (x) : dfoldrM (n+1) α f x = dfoldrM n (α ∘ succ) (f ·.succ) x >>= f 0 := dfoldr_succ .. theorem dfoldrM_eq_foldrM [Monad m] [LawfulMonad m] (f : (i : Fin n) → α → m α) (x : α) : dfoldrM n (fun _ => α) f x = foldrM n f x := by @@ -126,47 +101,44 @@ theorem dfoldl_eq_foldl (f : Fin n → α → α) (x : α) : simp only [dfoldl_succ, foldl_succ, Function.comp_apply, Function.comp_def] congr; simp only [ih] -/-! ### dfoldr -/ - -theorem dfoldr_loop_zero (f : (i : Fin n) → α i.succ → α i.castSucc) (x) : - dfoldr.loop n α f 0 (Nat.zero_lt_succ n) x = x := by - rw [dfoldr.loop] - -theorem dfoldr_loop_succ (f : (i : Fin n) → α i.succ → α i.castSucc) (h : i < n) (x) : - dfoldr.loop n α f (i+1) (Nat.add_lt_add_right h 1) x = - dfoldr.loop n α f i (Nat.lt_add_right 1 h) (f ⟨i, h⟩ x) := by - rw [dfoldr.loop] - -theorem dfoldr_loop (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (h : i+1 ≤ n+1) (x) : - dfoldr.loop (n+1) α f (i+1) (Nat.add_lt_add_right h 1) x = - f 0 (dfoldr.loop n (α ∘ succ) (f ·.succ) i h x) := by - induction i with - | zero => simp [dfoldr_loop_succ, dfoldr_loop_zero] - | succ i ih => rw [dfoldr_loop_succ _ h, dfoldr_loop_succ _ (Nat.succ_lt_succ_iff.mp h), - ih (Nat.le_of_succ_le h)]; rfl +/-! ### dfoldlM -/ -@[simp] theorem dfoldr_zero (f : (i : Fin 0) → α i.succ → α i.castSucc) (x) : - dfoldr 0 α f x = x := dfoldr_loop_zero .. +theorem dfoldlM_loop_lt [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (h : i < n) (x) : + dfoldlM.loop n α f i (Nat.lt_add_right 1 h) x = + (f ⟨i, h⟩ x) >>= (dfoldlM.loop n α f (i+1) (Nat.add_lt_add_right h 1)) := by + rw [dfoldlM.loop, dif_pos h] -theorem dfoldr_succ (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) : - dfoldr (n+1) α f x = f 0 (dfoldr n (α ∘ succ) (f ·.succ) x) := dfoldr_loop .. +theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) : + dfoldlM.loop n α f n (Nat.le_refl _) x = pure x := by + rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq] -theorem dfoldr_succ_last (f : (i : Fin (n+1)) → α i.succ → α i.castSucc) (x) : - dfoldr (n+1) α f x = dfoldr n (α ∘ castSucc) (f ·.castSucc) (f (last n) x) := by - induction n with - | zero => simp only [dfoldr_succ, dfoldr_zero, last, zero_eta] - | succ n ih => rw [dfoldr_succ, ih (α := α ∘ succ) (f ·.succ), dfoldr_succ]; congr +@[simp] theorem dfoldlM_zero [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x) : + dfoldlM 0 α f x = pure x := dfoldlM_loop_eq .. -theorem dfoldr_eq_dfoldrM (f : (i : Fin n) → α i.succ → α i.castSucc) (x) : - dfoldr n α f x = dfoldrM (m:=Id) n α f x := by - induction n <;> simp [dfoldr_succ, dfoldrM_succ, *] +theorem dfoldlM_loop [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (h : i < n+1) + (x) : dfoldlM.loop (n+1) α f i (Nat.lt_add_right 1 h) x = + f ⟨i, h⟩ x >>= (dfoldlM.loop n (α ∘ succ) (f ·.succ ·) i h .) := by + if h' : i < n then + rw [dfoldlM_loop_lt _ h _] + congr; funext + rw [dfoldlM_loop_lt _ h' _, dfoldlM_loop]; rfl + else + cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h') + rw [dfoldlM_loop_lt] + congr; funext + rw [dfoldlM_loop_eq, dfoldlM_loop_eq] -theorem dfoldr_eq_foldr (f : Fin n → α → α) (x : α) : dfoldr n (fun _ => α) f x = foldr n f x := by - induction n with - | zero => simp only [dfoldr_zero, foldr_zero] - | succ n ih => simp only [dfoldr_succ, foldr_succ, Function.comp_apply, Function.comp_def, ih] +theorem dfoldlM_succ [Monad m] (f : (i : Fin (n+1)) → α i.castSucc → m (α i.succ)) (x) : + dfoldlM (n+1) α f x = f 0 x >>= (dfoldlM n (α ∘ succ) (f ·.succ ·) .) := + dfoldlM_loop .. --- TODO: add `dfoldl_rev` and `dfoldr_rev` +theorem dfoldlM_eq_foldlM [Monad m] (f : (i : Fin n) → α → m α) (x : α) : + dfoldlM n (fun _ => α) f x = foldlM n (fun x i => f i x) x := by + induction n generalizing x with + | zero => simp only [dfoldlM_zero, foldlM_zero] + | succ n ih => + simp only [dfoldlM_succ, foldlM_succ, Function.comp_apply, Function.comp_def] + congr; ext; simp only [ih] /-! ### `Fin.fold{l/r}{M}` equals `List.fold{l/r}{M}` -/ From 7e2ecaca8e3641faafe70a79834cd3b6a8e26210 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Wed, 4 Dec 2024 11:53:49 -0300 Subject: [PATCH 14/14] added comment docstrings --- Batteries/Data/Fin/Basic.lean | 36 +++++++++++++++++++++++++++++------ 1 file changed, 30 insertions(+), 6 deletions(-) diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean index ef5a1f57f0..51fc68a28e 100644 --- a/Batteries/Data/Fin/Basic.lean +++ b/Batteries/Data/Fin/Basic.lean @@ -18,7 +18,10 @@ alias enum := Array.finRange @[deprecated (since := "2024-11-15")] alias list := List.finRange -/-- Dependent version of `Fin.foldr`. -/ +/-- Heterogeneous fold over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`, where +`f 2 : α 3 → α 2`, `f 1 : α 2 → α 1`, etc. + +This is the dependent version of `Fin.foldr`. -/ @[inline] def dfoldr (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.succ → α i.castSucc) (init : α (last n)) : α 0 := loop n (Nat.lt_succ_self n) init where @@ -29,12 +32,24 @@ alias list := List.finRange | i + 1 => loop i (Nat.lt_of_succ_lt h) (f ⟨i, Nat.lt_of_succ_lt_succ h⟩ x) | 0 => x -/-- Dependent version of `Fin.foldrM`. -/ +/-- Heterogeneous monadic fold over `Fin n` from right to left: +``` +Fin.foldrM n f xₙ = do + let xₙ₋₁ : α (n-1) ← f (n-1) xₙ + let xₙ₋₂ : α (n-2) ← f (n-2) xₙ₋₁ + ... + let x₀ : α 0 ← f 0 x₁ + pure x₀ +``` +This is the dependent version of `Fin.foldrM`, defined using `Fin.dfoldr`. -/ @[inline] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.succ → m (α i.castSucc)) (init : α (last n)) : m (α 0) := dfoldr n (fun i => m (α i)) (fun i x => x >>= f i) (pure init) -/-- Dependent version of `Fin.foldl`. -/ +/-- Heterogeneous fold over `Fin n` from the left: `foldl 3 f x = f 0 (f 1 (f 2 x))`, where +`f 0 : α 0 → α 1`, `f 1 : α 1 → α 2`, etc. + +This is the dependent version of `Fin.foldl`. -/ @[inline] def dfoldl (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.castSucc → α i.succ) (init : α 0) : α (last n) := loop 0 (Nat.zero_lt_succ n) init where @@ -46,16 +61,25 @@ alias list := List.finRange haveI : ⟨i, h⟩ = last n := by ext; simp; omega _root_.cast (congrArg α this) x -/-- Dependent version of `Fin.foldlM`. -/ +/-- Heterogeneous monadic fold over `Fin n` from left to right: +``` +Fin.foldlM n f x₀ = do + let x₁ : α 1 ← f 0 x₀ + let x₂ : α 2 ← f 1 x₁ + ... + let xₙ : α n ← f (n-1) xₙ₋₁ + pure xₙ +``` +This is the dependent version of `Fin.foldlM`. -/ @[inline] def dfoldlM [Monad m] (n : Nat) (α : Fin (n + 1) → Sort _) (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (init : α 0) : m (α (last n)) := loop 0 (Nat.zero_lt_succ n) init where /-- Inner loop for `Fin.dfoldlM`. ``` Fin.foldM.loop n α f i h xᵢ = do - let xᵢ₊₁ ← f i xᵢ + let xᵢ₊₁ : α (i+1) ← f i xᵢ ... - let xₙ ← f (n-1) xₙ₋₁ + let xₙ : α n ← f (n-1) xₙ₋₁ pure xₙ ``` -/