Interaction Trees

Interaction Trees (ITrees) are a coinductive datatype for representing recursive and impure programs that interact with an environment through a fixed set of events. We follow the construction of Xia, Zakowski, He, Hur, Malecha, Pierce, and Zdancewic, Interaction Trees: Representing Recursive and Impure Programs in Coq (POPL 2020), and adapt it to Lean 4 / Mathlib.

The Coq presentation defines

CoInductive itree (E : Type → Type) (R : Type) :=
| Ret (r : R) | Tau (t : itree E R) | Vis {X : Type} (e : E X) (k : X → itree E R).

In Lean we model the event signature as a polynomial functor F : PFunctor.{u, u} (shapes are event names, positions are answer types) so that the resulting tree lives at a single universe u. ITrees themselves are the M-type (final coalgebra) of the one-step polynomial functor Poly F α whose shapes are pure leaves, silent steps, or visible queries.

Naming conventions

Coq	Lean
itree E R	ITree F α
itreeF E R T	ITree.Shape F α
RetF / Ret	ITree.Shape.pure / ITree.pure
TauF / Tau	ITree.Shape.step / ITree.step
VisF / Vis	ITree.Shape.query / ITree.query
observe	ITree.shape
ITree.bind	ITree.bind (also >>=)
ITree.iter	ITree.iter
ITree.trigger e	ITree.lift

Main definitions

• ITree.Shape F α — one-step view of an ITree node.
• ITree.Poly F α — the polynomial functor whose M-type is ITree F α.
• ITree F α — interaction trees over events F with leaves of type α.
• ITree.pure, ITree.step, ITree.query — smart constructors.
• ITree.shape — one-step destructor, the analogue of Coq's observe.
• ITree.bind — monadic bind, defined via PFunctor.M.corec.
• ITree.iter — iteration combinator turning β → ITree F (β ⊕ α) into β → ITree F α, the canonical MonadIter operator.
• ITree.lift — lift a single event into an ITree: lift a = query a pure.
• Monad (ITree F), MonadIter (ITree F) — instances built from bind, pure, and iter.

Implementation notes

Lean 4's coinductive keyword (v4.25) only builds coinductive predicates; there is no built-in coinductive Type. We therefore use PFunctor.M, which is the standard Mathlib coinductive-type construction. The partial_fixpoint machinery is also not a substitute, because it requires a CCPO on the return type, which M F does not have. Corecursive functions producing ITrees go through PFunctor.M.corec. All of this is empirically validated in the project's ITreePilot.lean (no longer needed once this file is in place).

One-step polynomial functor

inductive ITree.Shape (F : PFunctor.{u, u}) (α : Type u) : Type u

One-step view of an ITree node: a pure leaf, a silent step, or a visible query. Mirrors Coq's itreeF (Core/ITreeDefinition.v).

• pure {F : PFunctor.{u, u}} {α : Type u} (r : α) : Shape F α

  A leaf carrying a result of type α. (Coq RetF.)

• step {F : PFunctor.{u, u}} {α : Type u} : Shape F α

  A silent (τ) step. (Coq TauF.)

• query {F : PFunctor.{u, u}} {α : Type u} (a : F.A) : Shape F α

  A visible event named by a : F.A; the continuation will be indexed by F.B a. (Coq VisF.)

@[reducible]

def ITree.Poly (F : PFunctor.{u, u}) (α : Type u) : PFunctor.{u, u}

One-step polynomial functor whose M-type is the type of ITrees over events F returning a value of type α.

• A := Shape F α: which kind of node we are at.
• B: the position type encoding the arity of each kind of node.
  • .pure r has no children (PEmpty).
  • .step has exactly one child (PUnit).
  • .query a has children indexed by the answer type F.B a.

def ITree (F : PFunctor.{u, u}) (α : Type u) : Type u

Interaction trees over events F : PFunctor.{u, u} with leaves of type α : Type u, defined as the final coalgebra (M-type) of ITree.Poly F α.

This is the Lean / Mathlib analogue of Coq's itree E R (InteractionTrees/theories/Core/ITreeDefinition.v).

Smart constructors

def ITree.pure {F : PFunctor.{u, u}} {α : Type u} (r : α) : ITree F α

Build the .pure ITree node carrying a result r : α. (Coq Ret.)

def ITree.step {F : PFunctor.{u, u}} {α : Type u} (t : ITree F α) : ITree F α

Build the .step ITree node — a silent step in front of t. (Coq Tau.)

def ITree.query {F : PFunctor.{u, u}} {α : Type u} (a : F.A) (k : F.B a → ITree F α) : ITree F α

Build the .query ITree node — a visible event a : F.A together with a continuation k : F.B a → ITree F α. (Coq Vis.)

One-step destructor (observe)

@[reducible]

def ITree.shape' {F : PFunctor.{u, u}} {α : Type u} (t : ITree F α) : ↑(Poly F α) (ITree F α)

One-step observation of an ITree as a Shape F α constructor packed with its continuation. Concretely a synonym for PFunctor.M.dest instantiated at Poly F α. (Coq observe.)

def ITree.shape {F : PFunctor.{u, u}} {α : Type u} (t : ITree F α) : Shape F α

One-step shape view of an ITree, dropping the continuation. The full data remains accessible via shape'.

@[simp]

theorem ITree.shape'_pure {F : PFunctor.{u, u}} {α : Type u} (r : α) : (pure r).shape' = ⟨Shape.pure r, PEmpty.elim⟩

@[simp]

theorem ITree.shape'_step {F : PFunctor.{u, u}} {α : Type u} (t : ITree F α) : t.step.shape' = ⟨Shape.step, fun (x : (Poly F α).B Shape.step) => t⟩

@[simp]

theorem ITree.shape'_query {F : PFunctor.{u, u}} {α : Type u} (a : F.A) (k : F.B a → ITree F α) : (query a k).shape' = ⟨Shape.query a, k⟩

@[simp]

theorem ITree.shape_pure {F : PFunctor.{u, u}} {α : Type u} (r : α) : (pure r).shape = Shape.pure r

@[simp]

theorem ITree.shape_step {F : PFunctor.{u, u}} {α : Type u} (t : ITree F α) : t.step.shape = Shape.step

@[simp]

theorem ITree.shape_query {F : PFunctor.{u, u}} {α : Type u} (a : F.A) (k : F.B a → ITree F α) : (query a k).shape = Shape.query a

def ITree.ofShape {F : PFunctor.{u, u}} {α : Type u} (sh : ↑(Poly F α) (ITree F α)) : ITree F α

Recover an ITree from its one-step shape together with the continuation data. The composition ofShape ∘ shape' = id and shape' ∘ ofShape = id hold definitionally (see ofShape_shape' and shape'_ofShape).

@[simp]

theorem ITree.shape'_ofShape {F : PFunctor.{u, u}} {α : Type u} (sh : ↑(Poly F α) (ITree F α)) : (ofShape sh).shape' = sh

@[simp]

theorem ITree.ofShape_shape' {F : PFunctor.{u, u}} {α : Type u} (t : ITree F α) : ofShape t.shape' = t

Monadic bind via M.corec

The Coq bind (Core/ITreeDefinition.v:157-168) is a cofix over subst. We translate it to M.corec by carrying a sum state: Sum.inl t means "we are still consuming the original tree t", Sum.inr u means "we have spliced in k r for some leaf r and are now propagating u's structure".

def ITree.bindStep {F : PFunctor.{u, u}} {α β : Type u} (k : α → ITree F β) : ITree F α ⊕ ITree F β → ↑(Poly F β) (ITree F α ⊕ ITree F β)

Step transformer used by bind: peel off one node from the current state and emit the corresponding output node together with the next state.

theorem ITree.bindStep_inl {F : PFunctor.{u, u}} {α β : Type u} (k : α → ITree F β) (t : ITree F α) : bindStep k (Sum.inl t) = match PFunctor.M.dest t with | ⟨Shape.pure r, snd⟩ => match PFunctor.M.dest (k r) with | ⟨s, c⟩ => ⟨s, fun (b : (Poly F β).B s) => Sum.inr (c b)⟩ | ⟨Shape.step, c⟩ => ⟨Shape.step, fun (x : (Poly F β).B Shape.step) => Sum.inl (c PUnit.unit)⟩ | ⟨Shape.query a, c⟩ => ⟨Shape.query a, fun (b : (Poly F β).B (Shape.query a)) => Sum.inl (c b)⟩

theorem ITree.bindStep_inr {F : PFunctor.{u, u}} {α β : Type u} (k : α → ITree F β) (u : ITree F β) : bindStep k (Sum.inr u) = match PFunctor.M.dest u with | ⟨s, c⟩ => ⟨s, fun (b : (Poly F β).B s) => Sum.inr (c b)⟩

def ITree.bind {F : PFunctor.{u, u}} {α β : Type u} (t : ITree F α) (k : α → ITree F β) : ITree F β

Monadic bind on ITrees. t.bind k runs t until it reaches a .pure r leaf and then continues with k r. (Coq ITree.bind.)

Iteration via M.corec

The Coq iter (Core/ITreeDefinition.v:192-194) is

CoFixpoint iter body i :=
  Tau (body i >>= fun rj => match rj with
                            | inl j => iter body j
                            | inr r => Ret r end).

Lean has no native guardedness checker, so the natural recursive form is rejected by both structural_recursion and partial_fixpoint. We therefore push the recursion into M.corec with state ITree F (β ⊕ α): at each step we peel off one node and convert leaves of the form .pure (.inl j) into a silent step followed by a fresh body j call.

def ITree.iterStep {F : PFunctor.{u, u}} {α β : Type u} (body : β → ITree F (β ⊕ α)) : ITree F (β ⊕ α) → ↑(Poly F α) (ITree F (β ⊕ α))

Step transformer used by iter.

def ITree.iter {F : PFunctor.{u, u}} {α β : Type u} (body : β → ITree F (β ⊕ α)) (init : β) : ITree F α

Iteration combinator. iter body init repeatedly invokes body : β → ITree F (β ⊕ α); intermediate Sum.inl j results restart the loop on j, intermediate Sum.inr r results terminate with r.

Each loop iteration is silent-step-guarded so the corecursive definition is productive. (Coq ITree.iter.)

Lifting events

def ITree.lift {F : PFunctor.{u, u}} (a : F.A) : ITree F (F.B a)

Lift a single event a : F.A into an ITree, returning the answer unchanged. (Coq ITree.trigger.)

Monad and MonadIter instances

@[implicit_reducible]

instance ITree.instMonad {F : PFunctor.{u, u}} : Monad (ITree F)

@[implicit_reducible]

instance ITree.instMonadIter {F : PFunctor.{u, u}} : MonadIter (ITree F)

Definitional unfoldings

These match Coq's Core/ITreeDefinition.v:208-217 (unfold_bind, unfold_iter) but as one-step simp lemmas on shape'. The full equational theory (bind_pure_left, bind_assoc, iter_unfold, …) requires bisimulation reasoning and lives in ToMathlib.ITree.Bisim.*.

@[simp]

theorem ITree.shape'_bind {F : PFunctor.{u, u}} {α β : Type u} (t : ITree F α) (k : α → ITree F β) : (t.bind k).shape' = (PFunctor.M.corec (bindStep k) (Sum.inl t)).dest

@[simp]

theorem ITree.shape'_iter {F : PFunctor.{u, u}} {α β : Type u} (body : β → ITree F (β ⊕ α)) (init : β) : (iter body init).shape' = (PFunctor.M.corec (iterStep body) (body init)).dest

@[simp]

theorem ITree.shape_lift {F : PFunctor.{u, u}} (a : F.A) : (lift a).shape = Shape.query a