Generalize `Fin.fold`?

Stream: batteries

[Quang Dao]

Lean currently defines docs#Fin.foldl and docs#Fin.foldr as special cases of the most general pattern possible. Something like:

def foldl' {n : ℕ} {α : Fin (n + 1) → Sort*} {β : Fin n → Sort*}
    (f : ∀ i, α i.castSucc → β i → α i.succ) (init : α 0)
    (v : (i : Fin n) → β i) : α (Fin.last n) := by
  induction n with
  | zero => exact init
  | succ n ih =>
    exact @ih (α ∘ Fin.succ) (β ∘ Fin.succ) (fun i a => f i.succ a)
      (f 0 init (v ⟨0, by omega⟩)) (fun i => v i.succ)

One can recover docs#Fin.foldl as the special case where α is constant, β := Fin n, and v = id.

I happen to need this generalization for my project. Is there any wider interest in replacing Fin.foldl with this general version? For type-checking convenience, one could then recover the current version as a non-dependent case (like Fin.append and Fin.addCases).

I don't see this used anywhere in Mathlib and only in Batteries, hence the choice of channel.

[François G. Dorais]

Is there an issue with using Sigma (or PSigma) instead of a dependent type?

[Edward van de Meent]

from the looks of it, the fold you're describing is not a fold over Fin n but a fold over (i:Fin n) -> b i.

[François G. Dorais]

Actually, the β is easily eliminated with fv : (i : Fin n) → α i.castSucc → α i.succ defined by fv i x := f i x (v i).

[François G. Dorais]

In other words, this is sufficiently general for the OP's purposes:

def foldl' {n : Nat} {α : Fin (n + 1) → Sort _}
  (f : ∀ i, α i.castSucc → α i.succ) (init : α 0) : α (Fin.last n)

[François G. Dorais]

The main issue, in my opinion, is whether replacing the dependent type α : Fin (n + 1) → Sort _ by a sigma type (i : Fin (n + 1)) × α i is a burden for the OP's use case.

[Edward van de Meent]

i imagine having OP's fold allows for compatibility with stuff like mathlibs' docs#Matrix.vecCons ecosystem

[Edward van de Meent]

btw, a sigma and pi type are not the same at all

[Edward van de Meent]

so i don't get what you want to replace with (i : Fin n) × β i or (i : Fin (n + 1)) × α i

[Quang Dao]

I'm not sure what the solution would look like using Sigma types. For my use case it's more convenient to think of objects to fold over as tuples (i : Fin n) → α i.

[François G. Dorais]

I'm hinting at the usual currying trick.

I'm thinking how I would implement foldl'. I would define f' : (i : Fin (n + 1)) × α i → (i : Fin (n + 1)) × α i as f' ⟨i, x⟩ := ⟨i+1, f i x⟩ when i < n (and rolling back to ⟨0, init⟩ otherwise, say). Then iterate n times starting with ⟨0, init⟩. Perhaps using Nat.fold or with a tailored tail-recursive loop.

[François G. Dorais]

I'm wondering if this alternative is easily implementable by the OP or whether we really need a library function to encapsulate this.

[Eric Wieser]

François G. Dorais said:

In other words, this is sufficiently general for the OP's purposes:

def foldl' {n : Nat} {α : Fin (n + 1) → Sort _}
  (f : ∀ i, α i.castSucc → α i.succ) (init : α 0) : α (Fin.last n)

What happens if we just replace docs#Fin.foldl with this?

[Quang Dao]

I think docs#Fin.foldl has a nice tail-recursive implementation right now. I'm trying to generalize that, but the final function may be less nice.

Also, note that Fin.foldl' is highly similar to Fin.hIterate, so that's where I'm trying to port the tail-recursive definition from. It's not similar enough to define the former in terms of the latter though (lots of type casting involved).

[Quang Dao]

Not very nice right now, but here's the adaptation:

import Mathlib

def foldCasesFrom {n} (P : Fin (n + 1) → Sort*)
    (f : ∀ (i : Fin n), P i.castSucc → P i.succ)
      (i : Fin (n + 1)) (a : P i) : P (last n) :=
  if h : i ≠ last n then
    haveI this : P (i + 1) := by simpa [succ_castPred_eq_add_one] using (f (i.castPred h) a)
    foldCasesFrom P f (i+1) this
  else
    _root_.cast (congrArg P (not_not.mp h)) a
  termination_by n - i
  decreasing_by
    have h0 : i < last n := lt_last_iff_ne_last.mpr h
    have h1 : i.val < n := by omega
    have h2 : (i + 1).val = i.val + 1 := by simp [val_add, h1]
    rw [h2]
    exact Nat.sub_add_lt_sub h1 (by omega)

def foldCases {n} (P : Fin (n + 1) → Sort*)
    (f : ∀(i : Fin n), P i.castSucc → P i.succ)
      (init : P 0) : P (last n) :=
  foldCasesFrom P f 0 init

[François G. Dorais]

Eric Wieser said:

François G. Dorais said:

In other words, this is sufficiently general for the OP's purposes:

def foldl' {n : Nat} {α : Fin (n + 1) → Sort _}
  (f : ∀ i, α i.castSucc → α i.succ) (init : α 0) : α (Fin.last n)

What happens if we just replace docs#Fin.foldl with this?

It's not a drop-in replacement. It would have to be Fin.depFoldl or something.

[François G. Dorais]

@Quang Dao Please make a draft PR to Batteries and we will work together on refining the implementation.

[Quang Dao]

It is now batteries#1071.

[Kim Morrison]

I've left some comments.

[François G. Dorais]

@Quang Dao I didn't think about this while reviewing batteries#1071 when you said you needed dfold{l/r} to use Sort _ and not Type _: is there a reason why you couldn't use Fin.induction, for example, to handle the Prop case in your application? I'm asking because there is no reason for induction principles to be efficient and we would save a bunch of code by defining dfoldl{l/r} in terms of their monadic versions.

[Quang Dao]

Yes, I think you're right. I haven't gotten to the part where I need to use Sort _ yet, but you can go ahead and make the change.

[François G. Dorais]

Great! If you have time, I would appreciate your review for batteries#1074