The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

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.