Coinductive interaction trees

This module defines the coinductive interaction tree ITree as the final coalgebra (PFunctor.M) of the interaction-tree polynomial functor, together with its constructors (ret, tau, vis), the dependent matcher dMatchOn, injectivity lemmas for the constructors, and the bisimulation equality IEq that is proven to coincide with propositional equality (ieq_iff_eq).

inductive Lean4Itree.ITree.shape (ε : Type u1 → Type v) (ρ : Type u2) : Type (max (max (u1 + 1) u2) v)

The node shapes of an interaction tree: a returned value, a silent tau step, or a visible effect vis. This is the A-component of the polynomial functor whose M-type is ITree.

• ret {ε : Type u1 → Type v} {ρ : Type u2} (v : ρ) : shape ε ρ
• tau {ε : Type u1 → Type v} {ρ : Type u2} : shape ε ρ
• vis {ε : Type u1 → Type v} {ρ : Type u2} (α : Type u1) (e : ε α) : shape ε ρ

def Lean4Itree.ITree.children {ε : Type u1 → Type v} {ρ : Type u2} : shape ε ρ → Type u1

The arity (B-component) of each interaction-tree node shape: a ret node has no children, a tau node has one, and a vis α e node has one child per inhabitant of the response type α.

Equations

• Lean4Itree.ITree.children (Lean4Itree.ITree.shape.ret v) = ULift.{?u.3, 0} (Fin2 0)
• Lean4Itree.ITree.children Lean4Itree.ITree.shape.tau = ULift.{?u.6, 0} (Fin2 1)
• Lean4Itree.ITree.children (Lean4Itree.ITree.shape.vis α e) = α

def Lean4Itree.ITree.P (ε : Type u1 → Type v) (ρ : Type u2) : PFunctor.{max (max u2 v) (u1 + 1), u1}

The interaction-tree polynomial functor, packaging shape and children.

Equations

• Lean4Itree.ITree.P ε ρ = { A := Lean4Itree.ITree.shape ε ρ, B := Lean4Itree.ITree.children }

def Lean4Itree.ITree (ε : Type u1 → Type v) (ρ : Type u2) : Type (max (max (max (u1 + 1) u2) v) u1)

Coinductive Interaction Tree defined with PFunctor.M. Equivalent to the following definition:

coinductive ITree (ε : Type → Type) (ρ : Type)
| ret (v : ρ)
| tau (t : ITree ε ρ)
| vis {α : Type} (e : ε α) (k : α → ITree ε ρ)

Equations

• Lean4Itree.ITree ε ρ = (Lean4Itree.ITree.P ε ρ).M

@[reducible, inline]

abbrev Lean4Itree.KTree (ε : Type u1 → Type v) (α : Type u1) (β : Type u2) : Type (max (max (max u1 u2) v) (u1 + 1))

A continuation tree: a function from α into interaction trees, i.e. a Kleisli arrow for the ITree monad.

Equations

• Lean4Itree.KTree ε α β = (α → Lean4Itree.ITree ε β)

@[implicit_reducible]

instance Lean4Itree.ITree.instOfNatChildrenTauZero {ε : Type u_1 → Type u_2} {ρ : Type u_3} : OfNat ((P ε ρ).B shape.tau) 0

Equations

• Lean4Itree.ITree.instOfNatChildrenTauZero = { ofNat := { down := Fin2.ofNat' 0 } }

def Lean4Itree.ITree.ret' {ε : Type u1 → Type v} {ρ : Type u2} {X : Type u} (v : ρ) : ↑(P ε ρ) X

One layer of a ret node in the polynomial functor: returns the value v.

Equations

• Lean4Itree.ITree.ret' v = ⟨Lean4Itree.ITree.shape.ret v, Lean4Itree.elim0⟩

def Lean4Itree.ITree.tau' {ε : Type u1 → Type v} {ρ : Type u2} {X : Type u} (t : X) : ↑(P ε ρ) X

One layer of a tau node in the polynomial functor: a single silent child t.

Equations

• Lean4Itree.ITree.tau' t = ⟨Lean4Itree.ITree.shape.tau, Lean4Itree.fin1Const t⟩

def Lean4Itree.ITree.vis' {ε : Type u1 → Type v} {ρ : Type u2} {X : Type u} {α : Type u1} (e : ε α) (k : α → X) : ↑(P ε ρ) X

One layer of a vis node in the polynomial functor: an effect e with continuation k indexed by the response type.

Equations

• Lean4Itree.ITree.vis' e k = ⟨Lean4Itree.ITree.shape.vis α e, fun (x : (Lean4Itree.ITree.P ε ρ).B (Lean4Itree.ITree.shape.vis α e)) => k x⟩

@[match_pattern]

def Lean4Itree.ITree.ret {ε : Type u1 → Type v} {ρ : Type u2} (v : ρ) : ITree ε ρ

The interaction tree that immediately returns the value v.

Equations

• Lean4Itree.ITree.ret v = PFunctor.M.mk (Lean4Itree.ITree.ret' v)

@[match_pattern]

def Lean4Itree.ITree.tau {ε : Type u1 → Type v} {ρ : Type u2} (t : ITree ε ρ) : ITree ε ρ

The interaction tree that takes one silent tau step into t.

Equations

• t.tau = PFunctor.M.mk (Lean4Itree.ITree.tau' t)

def Lean4Itree.ITree.tauN {ε : Type u1 → Type v} {ρ : Type u2} (n : ℕ) (t : ITree ε ρ) : ITree ε ρ

The interaction tree that takes n silent tau steps into t.

Equations

• Lean4Itree.ITree.tauN 0 t = t
• Lean4Itree.ITree.tauN n_2.succ t = (Lean4Itree.ITree.tauN n_2 t).tau

@[match_pattern]

def Lean4Itree.ITree.vis {ε : Type u1 → Type v} {ρ : Type u2} {α : Type u1} (e : ε α) (k : α → ITree ε ρ) : ITree ε ρ

The interaction tree that performs the effect e and continues with k.

Equations

• Lean4Itree.ITree.vis e k = PFunctor.M.mk (Lean4Itree.ITree.vis' e k)

def Lean4Itree.ITree.trigger {ε : Type u1 → Type v} {α : Type u1} (e : ε α) : ITree ε α

The interaction tree that performs the single effect e and returns its response.

Equations

• Lean4Itree.ITree.trigger e = Lean4Itree.ITree.vis e fun (x : α) => Lean4Itree.ITree.ret x

theorem Lean4Itree.ITree.ret_inj {ε : Type u1 → Type v} {ρ : Type u2} {x y : ρ} (h : ret x = ret y) : x = y

theorem Lean4Itree.ITree.vis_inj_α {ε : Type u_1 → Type u_2} {α1 α2 : Type u_1} {ρ : Type u_3} {k1 : KTree ε α1 ρ} {k2 : KTree ε α2 ρ} {e1 : ε α1} {e2 : ε α2} (h : vis e1 k1 = vis e2 k2) : α1 = α2

theorem Lean4Itree.ITree.vis_inj {ε : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_3} {e1 e2 : ε α} {k1 k2 : KTree ε α ρ} (h : vis e1 k1 = vis e2 k2) : e1 = e2 ∧ k1 = k2

theorem Lean4Itree.ITree.tau_inj {ε : Type u_1 → Type u_2} {ρ : Type u_3} {t1 t2 : ITree ε ρ} (h : t1.tau = t2.tau) : t1 = t2

def Lean4Itree.ITree.dMatchOn {ε : Type u1 → Type v} {ρ : Type u2} {motive : ITree ε ρ → Sort u} (x : ITree ε ρ) (ret : (v : ρ) → x = ret v → motive x) (tau : (c : ITree ε ρ) → x = c.tau → motive x) (vis : (α : Type u1) → (e : ε α) → (k : α → ITree ε ρ) → x = vis e k → motive x) : motive x

Custom dependent match function for ITrees

Equations

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

theorem Lean4Itree.ITree.dest_ret {ε : Type u1 → Type v} {ρ : Type u2} {v : ρ} : PFunctor.M.dest (ret v) = ⟨shape.ret v, elim0⟩

theorem Lean4Itree.ITree.dest_tau {ε : Type u1 → Type v} {ρ : Type u2} {t : ITree ε ρ} : PFunctor.M.dest t.tau = ⟨shape.tau, fin1Const t⟩

theorem Lean4Itree.ITree.dest_vis {ε : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_3} {e : ε α} {k : KTree ε α ρ} : PFunctor.M.dest (vis e k) = ⟨shape.vis α e, k⟩

def Lean4Itree.ITree.infTau {ε : Type u1 → Type v} {ρ : Type u2} : ITree ε ρ

Infinite Taus

Equations

• Lean4Itree.ITree.infTau = PFunctor.M.corec' (fun {X : Type (max (max (max (?u.3 + 1) ?u.1) ?u.2) ?u.3)} (rec : Unit → X) (x : Unit) => Sum.inr (Lean4Itree.ITree.tau' (rec x))) ()

theorem Lean4Itree.ITree.infTau_eq {ε : Type u1 → Type v} {ρ : Type u2} : infTau = infTau.tau

inductive Lean4Itree.ITree.State (ε : Type u1 → Type v1) (ρ : Type u2) : Type (max (max (u1 + 1) u2) v1)

A coinduction state for traversing interaction trees: either a whole tree (ct) or a continuation tree (kt).

• ct {ε : Type u1 → Type v1} {ρ : Type u2} : ITree ε ρ → State ε ρ
• kt {ε : Type u1 → Type v1} {ρ : Type u2} {α : Type u1} : KTree ε α ρ → State ε ρ

def Lean4Itree.ITree.«termC[_]» : Lean.ParserDescr

Notation C[ t ] for the tree state State.ct t.

Equations

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

def Lean4Itree.ITree.«termK[_]» : Lean.ParserDescr

Notation K[ t ] for the continuation-tree state State.kt t.

Equations

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

def Lean4Itree.ITree.«termK[_|_]» : Lean.ParserDescr

Notation K[ α | t ] for the continuation-tree state State.kt t with explicit index type α.

Equations

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

def Lean4Itree.ITree.tacticSimpItreeBasic : Lean.ParserDescr

Simplify basic interaction-tree constructors and PFunctor.M.dest_mk.

Equations

• Lean4Itree.ITree.tacticSimpItreeBasic = Lean.ParserDescr.node `Lean4Itree.ITree.tacticSimpItreeBasic 1024 (Lean.ParserDescr.nonReservedSymbol "simpItreeBasic" false)

def Lean4Itree.ITree.tacticSubstItreeInj_ : Lean.ParserDescr

Substitute the injectivity consequence of an equality h between interaction-tree constructors.

Equations

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

def Lean4Itree.ITree.tacticItree_elim_ : Lean.ParserDescr

itree_elim heq where heq is an equality between ITrees tries to to prove False using heq.

Equations

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

def Lean4Itree.ITree.tacticProveUnfoldLemma : Lean.ParserDescr

proveUnfoldLemma tries to finish a proof of an unfolding lemma defined by corec' Note you have to first unfold corec' in the appropriate places, possibly by some combination of conv and rw [PFunctor.M.unfold_corec'].

Equations

• Lean4Itree.ITree.tacticProveUnfoldLemma = Lean.ParserDescr.node `Lean4Itree.ITree.tacticProveUnfoldLemma 1024 (Lean.ParserDescr.nonReservedSymbol "proveUnfoldLemma" false)

inductive Lean4Itree.ITree.IEqF {ε : Type u1 → Type v} {ρ : Type u2} (sim : ITree ε ρ → ITree ε ρ → Prop) : ITree ε ρ → ITree ε ρ → Prop

One unfolding of the bisimulation functor: two interaction trees agree at the top constructor, with their immediate subtrees related by sim. The bisimulation equality IEq is the fixed point of IEqF.

• ret {ε : Type u1 → Type v} {ρ : Type u2} {sim : ITree ε ρ → ITree ε ρ → Prop} (v : ρ) : IEqF sim (ITree.ret v) (ITree.ret v)
• vis {ε : Type u1 → Type v} {ρ : Type u2} {sim : ITree ε ρ → ITree ε ρ → Prop} {α : Type u1} (e : ε α) (k1 k2 : α → ITree ε ρ) (h : ∀ (a : α), sim (k1 a) (k2 a)) : IEqF sim (ITree.vis e k1) (ITree.vis e k2)
• tau {ε : Type u1 → Type v} {ρ : Type u2} {sim : ITree ε ρ → ITree ε ρ → Prop} (t1 t2 : ITree ε ρ) (h : sim t1 t2) : IEqF sim t1.tau t2.tau

theorem Lean4Itree.ITree.IEqF_inv {ε : Type u1 → Type v} {ρ : Type u2} (sim : ITree ε ρ → ITree ε ρ → Prop) (t1 t2 : ITree ε ρ) (h : IEqF sim t1 t2) : (∃ (v : ρ), t1 = ret v ∧ t2 = ret v) ∨ (∃ (α : Type u1) (e : ε α) (k1 : α → ITree ε ρ) (k2 : α → ITree ε ρ), (∀ (a : α), sim (k1 a) (k2 a)) ∧ t1 = vis e k1 ∧ t2 = vis e k2) ∨ ∃ (t1' : ITree ε ρ) (t2' : ITree ε ρ), sim t1' t2' ∧ t1 = t1'.tau ∧ t2 = t2'.tau

theorem Lean4Itree.ITree.IEqF_monotone {ε : Type u1 → Type v} {ρ : Type u2} (sim sim' : ITree ε ρ → ITree ε ρ → Prop) (hsim : ∀ (t1 t2 : ITree ε ρ), sim t1 t2 → sim' t1 t2) (t1 t2 : ITree ε ρ) : IEqF sim t1 t2 → IEqF sim' t1 t2

@[irreducible]

def Lean4Itree.ITree.IEq {ε : Type u1 → Type v} {ρ : Type u2} (t1 t2 : ITree ε ρ) : Prop

Custom equality predicate between ITrees

Equations

• t1.IEq t2 = Lean4Itree.ITree.IEqF Lean4Itree.ITree.IEq t1 t2

theorem Lean4Itree.ITree.ieq_iff_eq {ε : Type u1 → Type v} {ρ : Type u2} (t1 t2 : ITree ε ρ) : t1.IEq t2 ↔ t1 = t2

theorem Lean4Itree.ITree.ieq_rfl {ε : Type u1 → Type v} {ρ : Type u2} {sim : ITree ε ρ → ITree ε ρ → Prop} {hsim : ∀ (t1 t2 : ITree ε ρ), t1.IEq t2 → sim t1 t2} (t : ITree ε ρ) : IEqF sim t t