Ignoring some event?

[alxest]

For a given itree (A +' B) R, I sometimes know that event A never occurs. So, I want to make it itree A R by ignoring event B. Is such function included in (or derivable from) the interaction tree library?

For now, I have defined one as below. But I would like to avoid using "cofix" (and proving coinductive proof).

Definition ignore_lF {A B R} (rec: itree (A +' B) R -> itree B R)
           (t : itreeF (A +' B) R _): itree B R  :=
  match t with
  | RetF x => Ret x
  | TauF t => Tau (rec t)
  | VisF e k => match e with
                | inl1 a => ITree.spin
                | inr1 b => Vis b (fun x => rec (k x))
                end
  end.

Definition ignore_l {A B R}
  : itree (A +' B) R -> itree B R
  := cofix ignore_l_ t := ignore_lF ignore_l_ (observe t).

[YaZko]

Hello,

There is nothing specific dedicated to this currently in the library, but that's definitely a sensible thing to have. Note however that in your approach you are using divergence (ITree.spin) to morally represent failure (there should not be a A in the tree). I think that the approach to follow would rather be:

• Define a coinductive predicate Has_no_A judging that a tree does not contain any A. Prove some structural rules that ease the proof that a given tree satisfies this predicate.
• Define the simple handler h_A_fails that translates A events into the Failure event from the library.
• Prove the following lemma: given a tree t, if Has_no_A t then eutt eq (interp h_A_fails t) t. I.e. state that if the predicate was true, then interpreting into failure the A events preserves bisimilarity.

Do you feel like such a sketch makes sense for your use case?

On a side note, this kinda feels like a particular case of the more general notion of contracts that the FreeSpec uses. Though I'm not sure whether we want to develop something similar as it is kinda redundant with the Dijkstra monad approach that Lucas and Steve are exploring.

[Lysxia]

@alxest's implementation looks reasonable; if you know a case doesn't happen it doesn't really matter how you handle it.

Instead of a manual cofix, this should be doable with interp:

Definition ignore_l {A B : Type -> Type} : itree (A +' B) ~> itree B :=
  interp (fun _ e =>
    match e with
    | inl1 _ => spin
    | inr1 er => trigger er
    end).

[YaZko]

Right, no need to carry failure in the type if failure won't happen, that's fair indeed!

[alxest]

Thank you for your kind replies!

@YaZko For proof structure, I think your sketch makes sense and I will do something similar to what you have suggested. For representing failure, I will try the "spin" approach and will let you know if something goes wrong. @Lysxia That is exactly what I wanted. Cool!

I will close the issue.