Open YaZko opened 2 years ago
YaZko
commented
2 years ago There appears to be a bug in the coinduction library that needs to be fixed before going forward with this issue: the coinduction tactic seems to fail its reification when the greatest fixed point is an heterogeneous relation (see https://github.com/damien-pous/coinduction/issues/5).
elefthei
commented
2 years ago I also have a use case for this feature -- making a note here for posterity :)
YaZko
commented
2 years ago I was planning on getting started on this Today, but got sidetracked slightly and am a bit hesitant as to what is the best pragmatic path.
As mentioned above, the necessary extension has been only recently added to the coinduction library. Damien went even further today by supporting not only heterogeneous relations (the only thing we need) but also heterogeneous dependent relations. However this complicates the unification problems that arise during typeclass resolution of setoid rewrites, and it has broken some of our code.
So I am basically hesitating between:
If I understand correctly the lack of this feature is straight up blocking for you @elefthei ? It's gonna soon be for @nchappe so the latter should probably be started now.
elefthei
commented
2 years ago I got unblocked! With a post-processing hack which is ugly but works for now :)
The current notion of bisimulation we use requires the computations to share the same signature of effects, and the same return type. This is reflected by the fact that the bisimulation checks that the challenges in the bisimulation game request to expose the same label, up-to coq's
eq.Relaxing this constraint on the return type is necessary to recover
eutt's flexibility, but @nchappe has already a use case where he needs the additional flexibility to relate syntactically distinct events.It should be slightly verbose but relatively straightforward to expand the current definition without breaking the current theory. Extending the theory should not be too bad, but a bit more work.