Monad structure on interaction trees

This module equips ITree with its functor and monad operations (map, bind, iter) and proves the lawful functor and monad instances, including bind_assoc, using the parameterized-coinduction (Paco) tactics.

def Lean4Itree.ITree.map {α : Type u_1} {β : Type u_2} {ε : Type u_3 → Type u_4} (f : α → β) (t : ITree ε α) : ITree ε β

Map the function f over the returned values of the interaction tree t.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean4Itree.ITree.instFunctor {ε : Type u_1 → Type u_2} : Functor (ITree ε)

Equations

• Lean4Itree.ITree.instFunctor = { map := fun {α β : Type ?u.1} => Lean4Itree.ITree.map }

theorem Lean4Itree.ITree.map_ret {α✝ : Type u_1} {ρ✝ : Type u_2} {f : α✝ → ρ✝} {v : α✝} {ε : Type u1 → Type v1} : map f (ret v) = ret (f v)

theorem Lean4Itree.ITree.map_tau {ρ : Type u_1} {ρ✝ : Type u_2} {f : ρ → ρ✝} {ε : Type u1 → Type v1} {c : ITree ε ρ} : map f c.tau = (map f c).tau

theorem Lean4Itree.ITree.map_vis {ρ : Type u_1} {σ : Type u_2} {ε : Type u1 → Type v1} {α : Type u1} {e : ε α} {k : α → ITree ε ρ} {f : ρ → σ} : map f (vis e k) = vis e fun (x : α) => map f (k x)

def Lean4Itree.ITree.bind {ε : Type u_1 → Type u_2} {ρ : Type u_3} {σ : Type u_4} (t : ITree ε ρ) (f : ρ → ITree ε σ) : ITree ε σ

Monadic bind: run t and feed each returned value into the continuation f.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean4Itree.ITree.instMonad {ε : Type u_1 → Type u_2} : Monad (ITree ε)

Equations

• One or more equations did not get rendered due to their size.

theorem Lean4Itree.ITree.bind_map {ε : Type u_1 → Type u_2} {α β : Type u_3} (f : ITree ε (α → β)) (x : ITree ε α) : (do let f ← f map f x) = f <*> x

theorem Lean4Itree.ITree.bind_ret {ρ✝ : Type u_1} {v : ρ✝} {ε✝ : Type u_2 → Type u_3} {ρ✝¹ : Type u_4} {f : ρ✝ → ITree ε✝ ρ✝¹} : (ret v).bind f = f v

theorem Lean4Itree.ITree.bind_tau {ε✝ : Type u_1 → Type u_2} {ρ✝ : Type u_3} {c : ITree ε✝ ρ✝} {ρ✝¹ : Type u_4} {f : ρ✝ → ITree ε✝ ρ✝¹} : c.tau.bind f = (c.bind f).tau

theorem Lean4Itree.ITree.bind_vis {ε✝ : Type u_1 → Type u_2} {a✝ : Type u_1} {e : ε✝ a✝} {ρ✝ : Type u_3} {k : a✝ → ITree ε✝ ρ✝} {ρ✝¹ : Type u_4} {f : ρ✝ → ITree ε✝ ρ✝¹} : (vis e k).bind f = vis e fun (x : a✝) => (k x).bind f

def Lean4Itree.ITree.tacticItree_eq_ : Lean.ParserDescr

itree_eq t tries to prove the equivalence of two ITrees transformed by map and bind.

t is the tree to be reverted

Equations

• One or more equations did not get rendered due to their size.

theorem Lean4Itree.ITree.id_map {ε : Type u_1 → Type u_2} {ρ : Type u_3} (t : ITree ε ρ) : map id t = t

theorem Lean4Itree.ITree.comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ε : Type u_4 → Type u_5} (g : α → β) (h : β → γ) (t : ITree ε α) : map (h ∘ g) t = map h (map g t)

instance Lean4Itree.ITree.instLawfulFunctor {ε : Type u_1 → Type u_2} : LawfulFunctor (ITree ε)

theorem Lean4Itree.ITree.map_const_left {α : Type u_1} {ρ✝ : Type u_2} {v : ρ✝} {ε✝ : Type u_3 → Type u_4} {t : ITree ε✝ α} : map (Function.const α v) t = t.bind fun (x : α) => ret v

theorem Lean4Itree.ITree.map_const_right {α : Sort u_1} {v : α} {ε✝ : Type u_2 → Type u_3} {ρ✝ : Type u_4} {t : ITree ε✝ ρ✝} : map (Function.const α id v) t = t

def Lean4Itree.ITree.tacticItree_eq_map_const__ : Lean.ParserDescr

itree_eq_map_const x y tries to prove the equivalence of two ITrees transformed by seq and map with Function.const.

x and y are the trees to be reverted

Equations

• One or more equations did not get rendered due to their size.

theorem Lean4Itree.ITree.seqLeft_eq {ε : Type u_1 → Type u_2} {α β : Type u_3} (x : ITree ε α) (y : ITree ε β) : x <* y = Function.const β <$> x <*> y

theorem Lean4Itree.ITree.seqRight_eq {ε : Type u_1 → Type u_2} {α β : Type u_3} (x : ITree ε α) (y : ITree ε β) : x *> y = Function.const α id <$> x <*> y

theorem Lean4Itree.ITree.pure_seq {α β : Type u_1} {ε : Type u_2 → Type u_3} (g : α → β) (x : ITree ε α) : pure g <*> x = g <$> x

theorem Lean4Itree.ITree.bind_pure_comp {α : Type u_1} {β : Type u_2} {ε : Type u_3 → Type u_4} (f : α → β) (x : ITree ε α) : x.bind (pure ∘ f) = map f x

theorem Lean4Itree.ITree.pure_bind {α : Type u_1} {ε : Type u_2 → Type u_3} {β : Type u_4} (x : α) (f : α → ITree ε β) : (pure x).bind f = f x

theorem Lean4Itree.ITree.bind_assoc {ε : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} (x : ITree ε α) (f : α → ITree ε β) (g : β → ITree ε γ) : (x.bind f).bind g = x.bind fun (x : α) => (f x).bind g

instance Lean4Itree.ITree.instLawfulMonad {ε : Type u_1 → Type u_2} : LawfulMonad (ITree ε)