Init.Data.Fin.Fold

Fin.foldl definition

(n) (f : α → Fin n → α) (init : α) : α

Full source

/--
Combine all the values that can be represented by `Fin n` with an initial value, starting at `0` and
nesting to the left.

Example:
 * `Fin.foldl 3 (· + ·.val) (0 : Nat) = ((0 + (0 : Fin 3).val) + (1 : Fin 3).val) + (2 : Fin 3).val`
-/
@[inline] def foldl (n) (f : α → Fin n → α) (init : α) : α := loop init 0 where
  /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
  @[semireducible, specialize] loop (x : α) (i : Nat) : α :=
    if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
  termination_by n - i

Left fold over finite natural numbers

Informal description

Given a natural number $n$, a function $f : \alpha \to \text{Fin } n \to \alpha$, and an initial value $x_0 : \alpha$, the function $\text{Fin.foldl}$ computes the left-fold of $f$ over all elements of $\text{Fin } n$ starting from $0$ up to $n-1$. More precisely, it computes $f(\cdots(f(f(x_0, 0), 1), \cdots), n-1)$, where each $i$ is treated as an element of $\text{Fin } n$ (i.e., $i < n$).

Fin.foldr definition

(n) (f : Fin n → α → α) (init : α) : α

Full source

/--
Combine all the values that can be represented by `Fin n` with an initial value, starting at `n - 1`
and nesting to the right.

Example:
 * `Fin.foldr 3 (·.val + ·) (0 : Nat) = (0 : Fin 3).val + ((1 : Fin 3).val + ((2 : Fin 3).val + 0))`
-/
@[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop n (Nat.le_refl n) init where
  /-- Inner loop for `Fin.foldr`. `Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))`  -/
  @[specialize] loop : (i : _) → i ≤ n → α → α
  | 0, _, x => x
  | i+1, h, x => loop i (Nat.le_of_lt h) (f ⟨i, h⟩ x)
  termination_by structural i => i

Right fold over finite natural numbers

Informal description

Given a natural number $n$, a function $f : \text{Fin } n \to \alpha \to \alpha$, and an initial value $x_0 : \alpha$, the function $\text{Fin.foldr}$ computes the right-fold of $f$ over all elements of $\text{Fin } n$ starting from $n-1$ down to $0$. More precisely, it computes $f(0, f(1, \cdots f(n-1, x_0)\cdots))$, where each $i$ is treated as an element of $\text{Fin } n$ (i.e., $i < n$).

Fin.foldlM definition

[Monad m] (n) (f : α → Fin n → m α) (init : α) : m α

Full source

/--
Folds a monadic function over all the values in `Fin n` from left to right, starting with `0`.

It is the sequence of steps:
```
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ₙ
  ```
  -/
  @[semireducible, specialize] 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
  decreasing_by decreasing_trivial_pre_omega

Monadic left fold over `Fin n`

Informal description

Given a monad `m`, a natural number `n`, a function `f : α → Fin n → m α`, and an initial value `init : α`, the function `Fin.foldlM` performs a left-fold over the finite set `Fin n` (from `0` up to `n-1`) using the monadic function `f`. More precisely, it computes the sequence: ``` do let x₁ ← f init 0 let x₂ ← f x₁ 1 ... let xₙ ← f xₙ₋₁ (n-1) pure xₙ ``` where each `i` is treated as an element of `Fin n` (i.e., `i < n`).

Fin.foldrM definition

[Monad m] (n) (f : Fin n → α → m α) (init : α) : m α

Full source

/--
Folds a monadic function over `Fin n` from right to left, starting with `n-1`.

It is the sequence of steps:
```
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₀
  ```
  -/
  @[semireducible, specialize] loop : {i // i ≤ n} → α → m α
  | ⟨0, _⟩, x => pure x
  | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩

Right monadic fold over `Fin n`

Informal description

Given a monad `m`, a natural number `n`, a function `f : Fin n → α → m α`, and an initial value `init : α`, the function `Fin.foldrM` performs a right-fold over the finite set `Fin n` (from `n-1` down to `0`) using the monadic function `f`. More precisely, it computes the sequence: ``` f (n-1) xₙ >>= f (n-2) · >>= ... >>= f 0 x₁ >>= pure ``` where `xₙ = init` and each `xᵢ` is the result of the previous monadic operation.

Fin.foldlM_loop_lt theorem

 [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))

Full source

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]

Recursive Relation for Monadic Left Fold on Finite Numbers When Index is Less Than Bound

Informal description

Let $m$ be a monad, $n$ be a natural number, and $f : \alpha \to \text{Fin}(n) \to m \alpha$ be a function. For any initial state $x : \alpha$ and index $i$ such that $i < n$, the monadic left fold operation satisfies the recursive relation: \[ \text{foldlM.loop}\ n\ f\ x\ i = f\ x\ \langle i, h \rangle \gg= \left(\lambda y, \text{foldlM.loop}\ n\ f\ y\ (i + 1)\right) \] where $\langle i, h \rangle$ denotes the element of $\text{Fin}(n)$ with value $i$ and proof $h$ that $i < n$, and $\gg=$ denotes the monadic bind operation.

Fin.foldlM_loop_eq theorem

[Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x

Full source

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 _)]

Monadic Left Fold Loop Base Case: $\text{foldlM.loop}\ n\ f\ x\ n = \text{pure}\ x$

Informal description

For any monad $m$, natural number $n$, function $f : \alpha \to \text{Fin}(n) \to m \alpha$, and initial value $x : \alpha$, the monadic left fold loop satisfies $\text{foldlM.loop}\ n\ f\ x\ n = \text{pure}\ x$.

Fin.foldlM_loop theorem

 [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)

Full source

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

Recursive Relation for Monadic Left Fold on Finite Numbers

Informal description

Let $m$ be a monad, $n$ be a natural number, and $f : \alpha \to \text{Fin}(n+1) \to m \alpha$ be a function. For any initial state $x : \alpha$ and index $i$ such that $i < n+1$, the monadic fold operation satisfies the recursive relation: \[ \text{foldlM.loop} (n+1) f x i = f x \langle i, h \rangle \gg= \left(\lambda y, \text{foldlM.loop} n (\lambda x j, f x j.\text{succ}) y i\right) \] where $\langle i, h \rangle$ denotes the element of $\text{Fin}(n+1)$ with value $i$ and proof $h$ that $i < n+1$, and $\gg=$ denotes the monadic bind operation.

Fin.foldlM_zero theorem

[Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x

Full source

@[simp] theorem foldlM_zero [Monad m] (f : α → Fin 0 → m α) (x) : foldlM 0 f x = pure x :=
  foldlM_loop_eq ..

Monadic Left Fold over Empty Finite Set Yields Pure Value

Informal description

For any monad $m$, any function $f : \alpha \to \text{Fin}(0) \to m \alpha$, and any initial value $x \in \alpha$, the monadic left fold over the empty finite set $\text{Fin}(0)$ satisfies $\text{foldlM}\ 0\ f\ x = \text{pure}\ x$.

Fin.foldlM_succ theorem

[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)

Full source

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 ..

Recursive relation for monadic left fold on $\text{Fin}(n+1)$

Informal description

Let $m$ be a monad and $f : \alpha \to \text{Fin}(n+1) \to m \alpha$ be a function. For any initial value $x \in \alpha$, the monadic left fold over $\text{Fin}(n+1)$ satisfies: \[ \text{foldlM}(n+1, f, x) = f(x, 0) \gg= \left( \lambda y, \text{foldlM}\left(n, \lambda z j, f(z, j.\text{succ}), y\right) \right) \] where $\gg=$ denotes the monadic bind operation and $j.\text{succ}$ is the successor operation on $\text{Fin}(n+1)$.

Fin.foldrM_loop_zero theorem

[Monad m] (f : Fin n → α → m α) (x) : foldrM.loop n f ⟨0, Nat.zero_le _⟩ x = pure x

Full source

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]

Base case of monadic right-fold loop: `foldrM.loop n f ⟨0, _⟩ x = pure x`

Informal description

For any monad `m`, any function `f : Fin n → α → m α`, and any initial value `x : α`, the monadic right-fold operation `foldrM.loop` evaluated at index `0` with proof `Nat.zero_le n` returns the pure value `x`.

Fin.foldrM_loop_succ theorem

 [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⟩

Full source

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]

Recursive Step of Monadic Right-Fold Loop on Finite Numbers

Informal description

Let $m$ be a monad, $f : \text{Fin}(n) \to \alpha \to m \alpha$ a function, $x : \alpha$ an initial value, and $i < n$ a natural number. Then the monadic right-fold loop satisfies the recursive relation: \[ \text{foldrM.loop}\ n\ f\ \langle i+1, h \rangle\ x = f\ \langle i, h \rangle\ x \gg= \text{foldrM.loop}\ n\ f\ \langle i, \text{Nat.le\_of\_lt}\ h \rangle \] where $\gg=$ denotes monadic bind and $\langle i, h \rangle$ represents a finite natural number $i$ with proof $h$ that $i < n$.

Fin.foldrM_loop theorem

 [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

Full source

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.loopfoldrM.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
    try simp only [foldrM.loop] -- the try makes this proof work with and without opaque wf rec
  | succ i ih =>
    rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
    congr; funext; exact ih ..

Recursive Relation for Monadic Right-Fold Loop on Successor-Bounded Finite Numbers

Informal description

Let $m$ be a monad and $f : \text{Fin}(n+1) \to \alpha \to m \alpha$ a function. For any initial value $x : \alpha$ and natural number $i$ such that $i+1 \leq n+1$, the monadic right-fold loop satisfies: \[ \text{foldrM.loop}\ (n+1)\ f\ \langle i+1, h \rangle\ x = \text{foldrM.loop}\ n\ (\lambda j, f\ j.\text{succ})\ \langle i, \text{Nat.le\_of\_succ\_le\_succ}\ h \rangle\ x \gg= f\ 0 \] where $\gg=$ denotes monadic bind and $\langle i, h \rangle$ represents a finite natural number $i$ with proof $h$ that $i < n+1$.

Fin.foldrM_zero theorem

[Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x

Full source

@[simp] theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x :=
  foldrM_loop_zero ..

Right Monadic Fold over Empty Finite Set Yields Pure Value

Informal description

For any monad `m`, any function `f : \text{Fin } 0 \to \alpha \to m \alpha`, and any initial value `x : \alpha`, the right monadic fold over the empty finite set `\text{Fin } 0` returns the pure value `x`.

Fin.foldrM_succ theorem

 [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

Full source

theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) :
    foldrM (n+1) f x = foldrMfoldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..

Recursive Relation for Right Monadic Fold on Successor-Bounded Finite Numbers

Informal description

Let $m$ be a monad and $f : \text{Fin}(n+1) \to \alpha \to m \alpha$ a function. For any initial value $x : \alpha$, the right monadic fold over $\text{Fin}(n+1)$ satisfies: \[ \text{foldrM}\ (n+1)\ f\ x = \text{foldrM}\ n\ (\lambda i, f\ i.\text{succ})\ x \gg= f\ 0 \] where $\gg=$ denotes monadic bind and $i.\text{succ}$ is the successor operation on $\text{Fin}(n+1)$.

Fin.foldl_loop_lt theorem

(f : α → Fin n → α) (x) (h : i < n) : foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i + 1)

Full source

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]

Recursive Step for Left-Fold Loop on Finite Numbers with $i < n$

Informal description

For any function $f : \alpha \to \text{Fin}\ n \to \alpha$, initial value $x \in \alpha$, and index $i < n$, the left-fold loop operation satisfies: \[ \text{foldl.loop}\ n\ f\ x\ i = \text{foldl.loop}\ n\ f\ (f\ x\ \langle i, h \rangle)\ (i + 1) \] where $\langle i, h \rangle$ denotes the element of $\text{Fin}\ n$ with value $i$ and proof $h$ that $i < n$.

Fin.foldl_loop_eq theorem

(f : α → Fin n → α) (x) : foldl.loop n f x n = x

Full source

theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x := by
  rw [foldl.loop, dif_neg (Nat.lt_irrefl _)]

Base Case of Left-Fold Loop on Finite Natural Numbers

Informal description

For any function $f : \alpha \to \text{Fin}(n) \to \alpha$ and initial value $x : \alpha$, the left-fold loop operation satisfies $\text{foldl.loop}(n, f, x, n) = x$.

Fin.foldl_loop theorem

 (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

Full source

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]

Recursive Relation for Left-Fold Loop on Finite Natural Numbers

Informal description

For any function $f : \alpha \to \text{Fin}(n+1) \to \alpha$, initial value $x \in \alpha$, and index $i$ with $i < n+1$, the left-fold loop operation satisfies the recursive relation: \[ \text{foldl.loop}(n+1, f, x, i) = \text{foldl.loop}\left(n, \lambda x j \mapsto f x (j.\text{succ}), f x \langle i, h \rangle, i\right) \] where $\langle i, h \rangle$ denotes the element of $\text{Fin}(n+1)$ with value $i$ and proof $h$ that $i < n+1$.

Fin.foldl_zero theorem

(f : α → Fin 0 → α) (x) : foldl 0 f x = x

Full source

@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x :=
  foldl_loop_eq ..

Left-Fold over Empty Finite Type Preserves Initial Value

Informal description

For any function $f : \alpha \to \text{Fin}(0) \to \alpha$ and initial value $x \in \alpha$, the left-fold operation over $\text{Fin}(0)$ satisfies $\text{foldl}(0, f, x) = x$.

Fin.foldl_succ theorem

(f : α → Fin (n + 1) → α) (x) : foldl (n + 1) f x = foldl n (fun x i => f x i.succ) (f x 0)

Full source

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 ..

Recursive Decomposition of Left-Fold over Successor Finite Type

Informal description

For any function $f : \alpha \to \text{Fin}(n+1) \to \alpha$ and initial value $x \in \alpha$, the left-fold operation over $\text{Fin}(n+1)$ satisfies: \[ \text{foldl}(n+1, f, x) = \text{foldl}\left(n, \lambda x i \mapsto f x (i.\text{succ}), f x 0\right) \] where $0$ denotes the zero element of $\text{Fin}(n+1)$ and $i.\text{succ}$ is the successor operation on $\text{Fin}(n+1)$.

Fin.foldl_succ_last theorem

(f : α → Fin (n + 1) → α) (x) : foldl (n + 1) f x = f (foldl n (f · ·.castSucc) x) (last n)

Full source

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]
  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]

Left-Fold Recursion via Cast-Successor and Last Element: $\text{foldl}(n+1, f, x) = f(\text{foldl}(n, f \circ \text{castSucc}, x), \text{last}(n))$

Informal description

For any function $f : \alpha \to \text{Fin}(n+1) \to \alpha$ and initial value $x \in \alpha$, the left-fold operation over $\text{Fin}(n+1)$ satisfies: \[ \text{foldl}(n+1, f, x) = f\left(\text{foldl}\big(n, \lambda y i \mapsto f y (i.\text{castSucc}), x\big), \text{last}(n)\right) \] where $i.\text{castSucc}$ is the canonical embedding of $\text{Fin}(n)$ into $\text{Fin}(n+1)$, and $\text{last}(n)$ is the maximal element of $\text{Fin}(n+1)$ (equal to $n$ as a natural number).

Fin.foldl_eq_foldlM theorem

(f : α → Fin n → α) (x) : foldl n f x = foldlM (m := Id) n f x

Full source

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, *]

Equivalence of Left-Fold and Identity Monadic Left-Fold over Finite Types

Informal description

For any function $f : \alpha \to \text{Fin}(n) \to \alpha$ and initial value $x \in \alpha$, the left-fold operation over $\text{Fin}(n)$ satisfies $\text{foldl}(n, f, x) = \text{foldlM}_{\text{Id}}(n, f, x)$, where $\text{foldlM}_{\text{Id}}$ denotes the monadic left-fold operation in the identity monad.

Fin.foldr_loop_zero theorem

(f : Fin n → α → α) (x) : foldr.loop n f 0 (Nat.zero_le _) x = x

Full source

theorem foldr_loop_zero (f : Fin n → α → α) (x) :
    foldr.loop n f 0 (Nat.zero_le _) x = x := by
  rw [foldr.loop]

Right-fold Loop Base Case: $\text{foldr.loop}\ n\ f\ 0\ h\ x = x$

Informal description

For any function $f : \text{Fin}\ n \to \alpha \to \alpha$ and initial value $x : \alpha$, the right-fold operation `foldr.loop` with starting index $0$ and proof of nonnegativity `Nat.zero_le` satisfies $\text{foldr.loop}\ n\ f\ 0\ (\text{Nat.zero\_le}\ n)\ x = x$.

Fin.foldr_loop_succ theorem

 (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)

Full source

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]

Recursive Step for Right-Fold Loop on Finite Numbers

Informal description

For any function $f : \text{Fin}\ n \to \alpha \to \alpha$, initial value $x : \alpha$, and index $i$ with proof $h : i < n$, the right-fold loop satisfies the recursive relation: \[ \text{foldr.loop}\ n\ f\ (i + 1)\ h\ x = \text{foldr.loop}\ n\ f\ i\ (\text{Nat.le\_of\_lt}\ h)\ (f\ \langle i, h \rangle\ x) \]

Fin.foldr_loop theorem

 (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)

Full source

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 with
  | zero => simp [foldr_loop_succ, foldr_loop_zero]
  | succ i ih => rw [foldr_loop_succ, ih]; rfl

Recursive Relation for Right-Fold Loop on Finite Numbers with Successor Function

Informal description

For any function $f : \text{Fin}(n+1) \to \alpha \to \alpha$, initial value $x : \alpha$, and index $i$ with proof $h : i + 1 \leq n + 1$, the right-fold loop satisfies: \[ \text{foldr.loop}\ (n+1)\ f\ (i+1)\ h\ x = f\ 0\ \left(\text{foldr.loop}\ n\ (\lambda j, f\ j.\text{succ})\ i\ (\text{Nat.le\_of\_succ\_le\_succ}\ h)\ x\right) \]

Fin.foldr_zero theorem

(f : Fin 0 → α → α) (x) : foldr 0 f x = x

Full source

@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x :=
  foldr_loop_zero ..

Right-fold over empty finite set equals identity

Informal description

For any function $f : \text{Fin}\ 0 \to \alpha \to \alpha$ and initial value $x : \alpha$, the right-fold operation $\text{foldr}$ satisfies $\text{foldr}\ 0\ f\ x = x$.

Fin.foldr_succ theorem

(f : Fin (n + 1) → α → α) (x) : foldr (n + 1) f x = f 0 (foldr n (fun i => f i.succ) x)

Full source

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 ..

Recursive Relation for Right-Fold on Successor of Finite Numbers

Informal description

For any natural number $n$, function $f : \text{Fin}(n+1) \to \alpha \to \alpha$, and initial value $x : \alpha$, the right-fold operation satisfies: \[ \text{foldr}\ (n+1)\ f\ x = f\ 0\ \left(\text{foldr}\ n\ (\lambda i, f\ i.\text{succ})\ x\right) \]

Fin.foldr_succ_last theorem

(f : Fin (n + 1) → α → α) (x) : foldr (n + 1) f x = foldr n (f ·.castSucc) (f (last n) x)

Full source

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]
  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]

Right-fold decomposition via last element and inclusion map

Informal description

For any natural number $n$, function $f : \text{Fin}(n+1) \to \alpha \to \alpha$, and initial value $x : \alpha$, the right-fold operation satisfies: \[ \text{foldr}\ (n+1)\ f\ x = \text{foldr}\ n\ (f \circ \text{castSucc})\ (f\ (\text{last}\ n)\ x) \] where $\text{castSucc} : \text{Fin}\ n \to \text{Fin}\ (n+1)$ is the inclusion map and $\text{last}\ n$ is the greatest element of $\text{Fin}\ (n+1)$.

Fin.foldr_eq_foldrM theorem

(f : Fin n → α → α) (x) : foldr n f x = foldrM (m := Id) n f x

Full source

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, *]

Equivalence of Right Fold and Right Monadic Fold with Identity Monad

Informal description

For any natural number $n$, function $f : \text{Fin } n \to \alpha \to \alpha$, and initial value $x : \alpha$, the right-fold operation $\text{foldr}$ is equivalent to the right monadic fold $\text{foldrM}$ with the identity monad. That is: \[ \text{foldr}\ n\ f\ x = \text{foldrM}\ n\ f\ x \] where the monad is taken to be the identity monad.

Fin.foldl_rev theorem

(f : Fin n → α → α) (x) : foldl n (fun x i => f i.rev x) x = foldr n f x

Full source

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]

Left-Fold with Reversed Indices Equals Right-Fold: $\text{foldl}_\text{rev} = \text{foldr}$

Informal description

For any natural number $n$, function $f : \text{Fin } n \to \alpha \to \alpha$, and initial value $x \in \alpha$, the left-fold operation with reversed indices satisfies: \[ \text{foldl}\ n\ (\lambda x i \mapsto f\ i.\text{rev}\ x)\ x = \text{foldr}\ n\ f\ x \] where $i.\text{rev}$ denotes the reversal of the index $i$ in $\text{Fin } n$ (i.e., $i.\text{rev} = n - (i + 1)$).

Fin.foldr_rev theorem

(f : α → Fin n → α) (x) : foldr n (fun i x => f x i.rev) x = foldl n f x

Full source

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]

Right-Fold with Reversed Indices Equals Left-Fold: $\text{foldr}_\text{rev} = \text{foldl}$

Informal description

For any natural number $n$, function $f : \alpha \to \text{Fin } n \to \alpha$, and initial value $x \in \alpha$, the right-fold operation with reversed indices satisfies: \[ \text{foldr}\ n\ (\lambda i\ x \mapsto f\ x\ i.\text{rev})\ x = \text{foldl}\ n\ f\ x \] where $i.\text{rev}$ denotes the reversal of the index $i$ in $\text{Fin } n$ (i.e., $i.\text{rev} = n - (i + 1)$).