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

hIterateFrom f i bnd a applies f over indices [i:n] to compute P n from P i.

See hIterate below for more details.

Equations

• Fin.hIterateFrom P f i ubnd a = if g : i < n then Fin.hIterateFrom P f (i + 1) g (f { val := i, isLt := g } a) else let_fun p := (_ : i = n); cast (_ : P i = P n) a

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

hIterate is a heterogenous iterative operation that applies a index-dependent function f to a value init : P start a total of stop - start times to produce a value of type P stop.

Concretely, hIterate start stop f init is equal to

  init |> f start _ |> f (start+1) _ ... |> f (end-1) _

Because it is heterogenous and must return a value of type P stop, hIterate requires proof that start ≤ stop.

One can prove properties of hIterate using the general theorem hIterate_elim or other more specialized theorems.

Equations

• Fin.hIterate P init f = Fin.hIterateFrom P f 0 (_ : 0 ≤ n) init

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

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