@[irreducible]

def Fin.hIterateFrom (P : Nat → Sort u_1) {n : Nat} (f : (i : Fin n) → P ↑i → P (↑i + 1)) (i : Nat) (ubnd : i ≤ n) (a : P i) : P n

Applies an index-dependent function f to all of the values in [i:n], starting at i with an initial accumulator a.

Concretely, Fin.hIterateFrom P f i a is equal to

  a |> f i |> f (i + 1) |> ... |> f (n - 1)

Theorems about Fin.hIterateFrom can be proven using the general theorem Fin.hIterateFrom_elim or other more specialized theorems.

Fin.hIterate is a variant that always starts at 0.

def Fin.hIterate (P : Nat → Sort u_1) {n : Nat} (init : P 0) (f : (i : Fin n) → P ↑i → P (↑i + 1)) : P n

Applies an index-dependent function to all the values less than the given bound n, starting at 0 with an accumulator.

Concretely, Fin.hIterate P init f is equal to

  init |> f 0 |> f 1 |> ... |> f (n-1)

Theorems about Fin.hIterate can be proven using the general theorem Fin.hIterate_elim or other more specialized theorems.

Fin.hIterateFrom is a variant that takes a custom starting value instead of 0.

theorem Fin.hIterate_elim {P : Nat → Sort u_1} (Q : (i : Nat) → P i → Prop) {n : Nat} (f : (i : Fin n) → P ↑i → P (↑i + 1)) (s : P 0) (init : Q 0 s) (step : ∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)) : Q n (hIterate P s f)

hIterate_elim provides a mechanism for showing that the result of hIterate satisfies a property Q stop by showing that the states at the intermediate indices i : start ≤ i < stop satisfy Q i.

theorem Fin.hIterate_eq {P : Nat → Sort u_1} (state : (i : Nat) → P i) {n : Nat} (f : (i : Fin n) → P ↑i → P (↑i + 1)) (s : P 0) (init : s = state 0) (step : ∀ (i : Fin n), f i (state ↑i) = state (↑i + 1)) : hIterate P s f = state n

hIterate_eqprovides a mechanism for replacing hIterate P s f with a function state showing that matches the steps performed by hIterate.

This allows rewriting incremental code using hIterate with a non-incremental state function.