Iteration of a partial self-map

Iterating a map α → Option α returns none as soon as one application is undefined. The bind composition law and the two successor equations support both recursive proofs and concatenation of partial trajectories. This supplies the common iteration used by crystal strings and path root operators.

def Option.iterate {α : Type u_1} (f : α → Option α) : ℕ → α → Option α

Apply a partial self-map n times, stopping at the first undefined value.

@[simp]

theorem Option.iterate_zero {α : Type u_1} (f : α → Option α) (x : α) : iterate f 0 x = some x

Zero iterations leave the starting value defined and unchanged.

theorem Option.iterate_succ {α : Type u_1} (f : α → Option α) (n : ℕ) (x : α) : iterate f (n + 1) x = (f x).bind (iterate f n)

First apply the partial map once, then perform the remaining iterations.

@[simp]

theorem Option.iterate_one {α : Type u_1} (f : α → Option α) (x : α) : iterate f 1 x = f x

A single iteration is the original partial map.

theorem Option.iterate_add {α : Type u_1} (f : α → Option α) (m n : ℕ) (x : α) : iterate f (m + n) x = (iterate f m x).bind (iterate f n)

Two successive runs of a partial map concatenate by option bind.

theorem Option.iterate_succ' {α : Type u_1} (f : α → Option α) (n : ℕ) (x : α) : iterate f (n + 1) x = (iterate f n x).bind f

A successor run can instead apply the partial map after the preceding iterations.