Question: Is this `Tau` essential?

[alxest]

(It is not a major hassle for me, but just out of curiosity.)

In the following Lemma,

Lemma unfold_interp_mrec R (t : itree (D +' E) R) :
  interp_mrec ctx t ≅ _interp_mrec (observe t).

Definition _interp_mrec {R : Type} (ot : itreeF (D +' E) R _) : itree E R :=
  match ot with
  | RetF r => Ret r
  | TauF t => Tau (interp_mrec ctx t)
  | VisF e k =>
    match e with
    | inl1 d => Tau (interp_mrec ctx (ctx _ d >>= k))
    | inr1 e => Vis e (fun x => Tau (interp_mrec ctx (k x)))
    end
  end.

I understand that we need to put additional Tau in the first event: Tau (interp_mrec ctx (ctx _ d >>= k)). However, I wonder if the Tau in the second event is essential: Vis e (fun x => Tau (interp_mrec ctx (k x))). Maybe this Tau was accidentally introduced when using ITree.iter?

[Lysxia]

Indeed that Tau gets inserted by iter. It could be avoided if we really wanted to but it's not a priority. One way would be to write a cofixpoint, but I've tried to minimize their usage. Another way would be to make iter more sophisticated to insert fewer Taus, but that complicates proofs. So I decided to live with those Taus.

[alxest]

@Lysxia That makes a lot of sense. Thanks for the clarification!

[Lysxia]

I added a comment about this in the source for posterity https://github.com/DeepSpec/InteractionTrees/commit/f8db33cc7663c8266be43ff4664d188b26cf1873