Interaction Trees in Lean 4

Interaction trees allow expressing potentially non-terminating and effectful programs. The core data structure is the following coinductive type:

coinductive ITree (E : Type -> Type) (R : Type) : Type
| ret : R         -> ITree E R
| tau : ITree E R -> ITree E R
| vis : {A : Type} -> E A -> (A -> ITree E R) -> ITree E R

ITree E forms a monad additionally equipped with iter. We can thus use do-notation:

def main : ITree (Mem & AssumeAssert) Nat := do
  let x <- Mem.read "x"
  assume (x < 10)
  return x

ITree Specifications

In order to be able to express constructs such as assume _; in intermediate verification languages such as Boogie 2, Dijkstra monads for ITrees can be used.

Next Up

• Not universe-polymorphic, which prevents us from implementing interp.
• A lot of coinductive theorems are missing.
• We assume that Quotienting ITrees along Eutt is possible, see QITree.lean.