Effect-free ForIn containers

PureForIn and PureForIn' identify the containers whose loop produces its elements without effects, so that iterating is iterating over the list ForIn.toList computes in Id, and LawfulMemForInId identifies those whose Membership agrees with that Id loop.

class Std.Internal.LawfulMemForInId (ρ : Type w) (α : Type u₁) [d : Membership α ρ] [ForIn Id ρ α] : Prop

Containers whose Membership is exactly the elements the Id loop enumerates. The Iff says the loop yields all members and nothing else; it constrains neither their order nor their multiplicity.

• mem_toList_iff {a : α} {xs : ρ} : a ∈ ForIn.toList xs ↔ a ∈ xs

  The elements of ForIn.toList xs are the members of xs.

class Std.Internal.PureForIn (m : Type u → Type v) (ρ : Type w) (α : Type u₁) [Monad m] [ForIn m ρ α] [ForIn Id ρ α] : Prop

Containers whose ForIn loop produces its elements without effects in m, so iterating over xs is iterating over the list ForIn.toList computes in Id. Only the loop body may have effects.

• forIn_eq {β : Type u} (xs : ρ) (init : β) (f : α → β → m (ForInStep β)) : forIn xs init f = forIn (ForIn.toList xs) init f

  Iterating over xs is iterating over ForIn.toList xs.

class Std.Internal.PureForIn' (m : Type u → Type v) (ρ : Type w) (α : Type u₁) [Monad m] {d : Membership α ρ} [ForIn' m ρ α d] [ForIn Id ρ α] [LawfulMemForInId ρ α] : Prop

Containers whose ForIn' loop produces its elements without effects in m, carrying a membership proof for each.

• forIn'_eq {β : Type u} (xs : ρ) (init : β) (f : (a : α) → a ∈ xs → β → m (ForInStep β)) : forIn' xs init f = forIn' (ForIn.toList xs) init fun (a : α) (h : a ∈ ForIn.toList xs) (b : β) => f a ⋯ b

  Iterating over xs is iterating over ForIn.toList xs.

theorem Std.Internal.foldl_push_toList {γ : Type u₁} (xs : List γ) (acc : Array γ) : (List.foldl (fun (acc : Array γ) (a : γ) => acc.push a) acc xs).toList = acc.toList ++ xs

Every element ForIn.toList collects is pushed onto the accumulator in order.

theorem Std.Internal.ForIn.toList_eq_of_forIn_eq {ρ : Type w} {α : Type u₁} [ForIn Id ρ α] {xs : ρ} {l : List α} (h : ∀ (init : Array α) (f : α → Array α → Id (ForInStep (Array α))), forIn xs init f = forIn l init f) : ForIn.toList xs = l

Computes ForIn.toList from the container's own equation between its loop and the loop over l.