[Coq-Club] New Co-inductive Restrictions

[Gregory Malecha]

Hello --

I wanted to ask about the new restrictions on co-inductives. I am trying to
update the interaction trees repository to work with the new restrictions
and I think I've done it correctly, but it seemed a little bit more verbose
than I was anticipating and so I'm wondering if there is a better way to do
it.

The full pull request is here:
https://github.com/DeepSpec/InteractionTrees/pull/26

Essentially the type that was

CoInductive itree (e : Type -> Type) (t : Type) : Type :=
| Ret (_ : t)
| Vis {u} (_ : e t) (_ : u -> itree e t)
| Tau (_ : itree e t).

Has become

Inductive itreeF (itree : Type) (e : Type -> Type) (t : Type) : Type :=
| RetF (_ : t)
| VisF {u} (_ : e t) (_ : u -> itree)
| Tau (_ : itree).

CoInductive itree (e : Type -> Type) (t : Type) : Type :=
{ observe : itreeF (itree e t) e t }.

This makes a lot of sense, the relations work similarly, but the tend to be
a bit more verbose. Essentially, they all get wrapped in something that
looks like:

Inductive EqF (r : relation (itree e t)) : itreeF (itree e t) e t -> itreeF
(itree e t) -> Prop :=
| eq_ret {x} : EqF r (RetF x) (RetF x)
| eq_vis {u} {y : e u} k1 k2}
(_ : forall x : u, r (k1 x) (k2 x))
: EqF r (VisF y k1) (VisF y k2)
| eq_tau {it1 it2}
(_ : r it1 it2)
: EqF r (TauF it1) (TauF it2)

CoInductive Eq (a b : itree e t) : Prop :=
{ observe_eq : EqF a.(observe) b.(observe) }.

Originally, I tried to write this without the observe in the type of Eq
(i.e. eq_ret would have type "forall x, EqF r {| observe := RetF x |} {|
observe := RetF x |}"), but this doesn't seem to work because the
constructors of this form are not helpful unless you can destruct a
co-inductive which is the problem being addressed by the new restriction.

So, back to the original question, is there a better (more convenient) way
to represent this type?

Thanks for any feedback.