Interaction trees (ITrees) give a general-purpose data structure
in Coq for formalizing the behaviors of recursive programs that
interact with their environment. In order to permit infinite
behaviors, ITrees are naturally defined as coinductive trees
thereby requiring coinductive reasoning.

In this talk, I will present an interesting coinductive proof
structure for reasoning about equivalence up to taus (i.e., silent
steps) between ITrees. The proofs can simultaneously carry two
coinductive structures: weaker coinduction hypotheses guarded by
any (silent or visible) steps, and stronger ones guarded by only
visible steps. Interestingly, the weaker hypotheses do not survive
under rewrites up to silent steps, while the stronger ones do.

I will also talk about how to mechanize the proof structure in Coq
using the Paco library, which provides general coinduction
principles and Coq tactics.