ITree.Simple

Simplified interface



Core definitions

Reexported from the library.

Require Export ITree.Core.ITreeDefinition.
Export ITreeNotations.
#[global] Open Scope itree_scope.
(* This scope is open by default to make this "tutorial module" as
   straightforward as possible. *)

The main functions are meant to be imported qualified, e.g., ITree.bind, ITree.trigger, to avoid ambiguity with identifiers of the same name (some of which are overloaded generalizations of these).
Indexed types
Require Export ITree.Basics.Basics.
  • Notation "E ~> F" := (∀ T, E T → F T)

Require Export ITree.Indexed.Sum.

Interpreters, handlers


Require Export ITree.Interp.Interp.

Require Export ITree.Interp.Recursion.

Require ITree.Interp.Handler.
Export ITree.Interp.Handler.Handler.
Combinators for event handlers:

Equational theory


Module Type SimpleTheory.
This interface is implemented by the module ITree.Simple.Simple below (exported by default).

Section EquivalenceUpToTaus.

Context {E : Type → Type} {R : Type}.

The standard itree equivalence: "Equivalence Up To Taus" (eutt for short), or weak bisimulation.
Parameter eutt : itree E R → itree E R → Prop.

Infix "≈" := eutt (at level 70) : type_scope.

eutt is an equivalence relation.
#[global] Declare Instance Equivalence_eutt :
    Equivalence eutt.

We can erase taus unter eutt.
Parameter tau_eutt : ∀ (t : itree E R),
    Tau t ≈ t.

Parameter itree_eta : ∀ (t : itree E R),
    t ≈ go (observe t).

Parameter eutt_ret : ∀ (r1 r2 : R),
    r1 = r2 → Ret r1 ≈ Ret r2.

Parameter eutt_vis : ∀ {U : Type} (e : E U) (k1 k2 : U → itree E R),
    (∀ u, k1 u ≈ k2 u) → Vis e k1 ≈ Vis e k2.

Parameter eutt_inv_ret : ∀ (r1 r2 : R),
    Ret r1 ≈ Ret r2 → r1 = r2.

Parameter eutt_inv_vis : ∀ {U : Type} (e : E U) (k1 k2 : U → itree E R),
     Vis e k1 ≈ Vis e k2 → (∀ u, k1 u ≈ k2 u).

End EquivalenceUpToTaus.

Infix "≈" := eutt (at level 70).

Rewriting lemmas


Parameter bind_ret : ∀ {E R S} (r : R) (k : R → itree E S),
    ITree.bind (Ret r) k ≈ k r.

Parameter bind_vis
  : ∀ {E R} U V (e: E V) (ek: V → itree E U) (k: U → itree E R),
    ITree.bind (Vis e ek) k
  ≈ Vis e (fun x ⇒ ITree.bind (ek x) k).

Parameter bind_ret_r : ∀ {E R} (s : itree E R),
    ITree.bind s (fun x ⇒ Ret x) ≈ s.

Parameter bind_bind
  : ∀ {E R S T}
           (s : itree E R) (k : R → itree E S) (h : S → itree E T),
    ITree.bind (ITree.bind s k) h
  ≈ ITree.bind s (fun r ⇒ ITree.bind (k r) h).

Hint Rewrite @tau_eutt : itree.
Hint Rewrite @bind_ret : itree.
Hint Rewrite @bind_vis : itree.
Hint Rewrite @bind_ret_r : itree.
Hint Rewrite @bind_bind : itree.

Monadic interpretation: interp


Definition _interp {E F R} (f : E ~> itree F) (ot : itreeF E R _)
  : itree F R
  := match ot with
     | RetF r ⇒ Ret r
     | TauF t ⇒ Tau (interp f t)
     | VisF e k ⇒ f _ e >>= (fun x ⇒ Tau (interp f (k x)))
     end.

Parameter unfold_interp
  : ∀ {E F R} {f : E ~> itree F} (t : itree E R),
    interp f t ≈ (_interp f (observe t)).

The next three are immediate corollaries of unfold_interp.
Parameter interp_ret
  : ∀ {E F R} {f : E ~> itree F} (x: R),
    interp f (Ret x) ≈ Ret x.

Parameter interp_vis
  : ∀ {E F R} {f : E ~> itree F} U (e: E U) (k: U → itree E R),
    interp f (Vis e k)
  ≈ ITree.bind (f _ e) (fun x ⇒ interp f (k x)).

Parameter interp_trigger : ∀ {E F : Type → Type} {R : Type}
      (f : E ~> (itree F)) (e : E R),
    interp f (ITree.trigger e) ≈ f _ e.

Parameter interp_bind : ∀ {E F R S}
      (f : E ~> itree F) (t : itree E R) (k : R → itree E S),
    interp f (ITree.bind t k)
  ≈ ITree.bind (interp f t) (fun r ⇒ interp f (k r)).

Hint Rewrite @interp_ret : itree.
Hint Rewrite @interp_vis : itree.
Hint Rewrite @interp_trigger : itree.
Hint Rewrite @interp_bind : itree.

Simple recursion: rec

rec body is equivalent to interp (recursive body), where recursive is defined as follows.
Definition recursive {E A B} (f : A → itree (callE A B +' E) B)
  : (callE A B +' E) ~> itree E
  := case_ (calling' (rec f)) ITree.trigger.

Parameter rec_as_interp
  : ∀ {E A B} (f : A → itree (callE A B +' E) B) (a : A),
    rec f a
  ≈ interp (recursive f) (f a).

Parameter interp_recursive_call
  : ∀ {E A B} (f : A → itree (callE A B +' E) B) (x : A),
    interp (recursive f) (call x)
  ≈ rec f x.

mrec ctx is equivalent to interp (mrecursive ctx), where mrecursive is defined as follows.
Definition mrecursive {D E} (f : D ~> itree (D +' E))
  : (D +' E) ~> itree E :=
  case_ (mrec f) ITree.trigger.

Parameter mrec_as_interp
  : ∀ {D E T} (ctx : D ~> itree (D +' E)) (d : D T),
    mrec ctx d
  ≈ interp (mrecursive ctx) (ctx _ d).

Parameter interp_mrecursive
  : ∀ {D E T} (ctx : D ~> itree (D +' E)) (d : D T),
    interp (mrecursive ctx) (trigger_inl1 d)
  ≈ mrec ctx d.

Hint Rewrite @interp_recursive_call : itree.
Hint Rewrite @interp_mrecursive : itree.

Proper lemmas


#[global]
Declare Instance eutt_go {E R} :
  Proper (going eutt ==> eutt) (@go E R).

#[global]
Declare Instance eutt_observe {E R} :
  Proper (eutt ==> going eutt) (@observe E R).

#[global]
Declare Instance eutt_TauF {E R} :
  Proper (eutt ==> going eutt) (@TauF E R _).

#[global]
Declare Instance eutt_VisF {E R X} (e: E X) :
  Proper (pointwise_relation _ (@eutt E R) ==> going eutt) (VisF e).

#[global]
Declare Instance eutt_bind {E R S} :
  Proper (eutt ==> pointwise_relation _ eutt ==> eutt)
         (@ITree.bind E R S).

#[global]
Declare Instance eutt_map {E R S} :
  Proper (pointwise_relation _ eq ==> eutt ==> eutt)
         (@ITree.map E R S).

#[global]
Declare Instance eutt_interp (E F : Type → Type) f (R : Type) :
  Proper (eutt ==> eutt) (@interp E (itree F) _ _ _ f R).

Tactics

Remove all taus from the left hand side of the goal (assumed to be of the form lhs ≈ rhs).
Ltac tau_steps :=
  repeat (
      rewrite itree_eta at 1; cbn;
      match goal with
      | [ |- go (observe _) ≈ _ ] ⇒ fail 1
      | _ ⇒ try rewrite tau_eutt
      end).

End SimpleTheory.