feat: Define dependent version of Fin.foldl

[quangvdao]

This PR defines the dependent versions of Fin.fold{l/r}{M}. This is 4 functions in total, Fin.dfold{l/r}{M}, and we give similar theorems as the non-dependent versions, plus theorems that relate the dependent to the non-dependent version.

Two theorems are currently missing: dfold{l/r}_rev. Even stating these theorems is a pain due to casting, so I'd prefer to add them later.

[kim-em]

Can you write the theorem relating it to the usual Fin.fold, with \alpha := \Sigma i, \alpha i?

[kim-em]

Other directions that would be good:

• just as we have Fin.fold and Nat.fold and a theorem relating them, we should have the "unbundled" version of this for Nat, and the theorem
• we should have the monadic version as well.

[quangvdao]

Can you write the theorem relating it to the usual Fin.fold, with \alpha := \Sigma i, \alpha i?

Actually, I don't know how to state the theorem. A natural attempt is:

theorem fold_eq_foldl_sigma {α : Fin (n+1) → Sort _} (f : ∀ (i : Fin n), α i.castSucc → α i.succ)
    (x : α 0) :
    fold n α f x = foldl n (α := (i : Fin (n + 1)) × α i) (fun x i => f x.1 x.2) ⟨0, x⟩ := sorry

but we run into the problem of Lean not knowing that x.1 is supposed to be the same as i.castSucc during execution.

[quangvdao]

• just as we have Fin.fold and Nat.fold and a theorem relating them, we should have the "unbundled" version of this for Nat, and the theorem

• I agree, though not quite sure where to put things (Data/Nat/Basic and Data/Nat/Lemmas, or a new Data/Nat/Fold).
• The dependent version of Nat.fold is Fin.hIterate.
• I can't find the lemma relating the current Fin.foldl with Nat.fold.

• we should have the monadic version as well.

This has been added.

As written, these new dependent versions add no overhead after compilation (some initial experiments also confirm this). Because of this, do you think we could redefine (say) Fin.foldl as the dependent version of Fin.fold?

Also, in terms of naming, I think writing Fin.fold and Fin.foldRev will align with the Nat version. And I'd also want to change the function signature in Fin.foldl:

Fin.foldl.{u_1} {α : Sort u_1} (n : ℕ) (f : α → Fin n → α) (init : α) : α

to

Fin.foldl.{u_1} {α : Sort u_1} (n : ℕ) (f : Fin n → α → α) (init : α) : α

in order to match the dependent version.

In summary, we can have Fin.fold' as the dependent version, Fin.fold as non-dependent, defined in terms of the former, the foldRev versions, and the monadic versions.

[fgdorais]

foldl and foldr are standard names in functional programming, we should stick to that convention. Use dfoldl/dfoldr or foldlDep/foldrDep.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1071 has successfully built against this PR. (2024-12-02 23:19:35) View Log
• ✅ Mathlib branch batteries-pr-testing-1071 has successfully built against this PR. (2024-12-03 01:09:49) View Log
• ✅ Mathlib branch batteries-pr-testing-1071 has successfully built against this PR. (2024-12-03 19:19:51) View Log
• ✅ Mathlib branch batteries-pr-testing-1071 has successfully built against this PR. (2024-12-04 01:46:51) View Log
• ✅ Mathlib branch batteries-pr-testing-1071 has successfully built against this PR. (2024-12-04 02:29:33) View Log
• ✅ Mathlib branch batteries-pr-testing-1071 has successfully built against this PR. (2024-12-04 16:25:39) View Log

[fgdorais]

@kim-em could you protect Fin.cast in Lean 4 when you have time? The few _root_.cast uses here are annoying.

[fgdorais]

Looks good. Make sure to add specialize on the inner loops. If you have time, expand the docstrings using Init.Data.Fin.Fold as a model. I'll have another pass tomorrow after a good night of sleep!

[fgdorais]

Avoid code duplication by defininig:

@[inline] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Type _)
    (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)

I'm not sure the same works for dfoldlM.

[quangvdao]

Avoid code duplication by defininig:

@[inline] def dfoldrM [Monad m] (n : Nat) (α : Fin (n + 1) → Type _)
    (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)

I'm not sure the same works for dfoldlM.

When I tried to do this, the theorems can't seem to infer the type of α and x.

[fgdorais]

The loop lemmas are no longer relevant after this change. The other lemmas are immediate consequences of the dfoldr lemmas.

[fgdorais]

I completed the last few changes for you. Let me know if you would like to revert something.

[fgdorais]

I just approved but I then noticed that the docstrings should not just refer to other functions. Please expand them and mention the relation with non-dependent functions as an additional note.

[quangvdao]

I filled out the docstrings. Thanks for all the help!

[kim-em]

@kim-em could you protect Fin.cast in Lean 4 when you have time? The few _root_.cast uses here are annoying.

Done in leanprover/lean4#6315