I've had to abandon the use of coqrel for now, because it makes rewriting somewhat unpredictable, and very, very slow. I've switched back to the dead simple definition of Relation that I was using previously, and all the speed came back.
If you'd like to take a look at my project, it's here: https://github.com/jwiegley/bytestring-fiat. Just replace the inclusion of Here.Relations with CoqRel.LogicalRelations. It's modules like FunMaps.v that really get slow, or in some cases, the proofs don't go through at all.
For a while I was working around it in various ways, especially by defining Morphisms.Proper instances rather than coqrel's new definition for Proper, but something else is interacting badly with the way that typeclass lookup should happen for rewrites.
I don't know yet what the problem is, just letting you know that it exists. :)
I've had to abandon the use of
coqrelfor now, because it makes rewriting somewhat unpredictable, and very, very slow. I've switched back to the dead simple definition ofRelationthat I was using previously, and all the speed came back.If you'd like to take a look at my project, it's here: https://github.com/jwiegley/bytestring-fiat. Just replace the inclusion of
Here.RelationswithCoqRel.LogicalRelations. It's modules likeFunMaps.vthat really get slow, or in some cases, the proofs don't go through at all.For a while I was working around it in various ways, especially by defining
Morphisms.Properinstances rather than coqrel's new definition forProper, but something else is interacting badly with the way that typeclass lookup should happen for rewrites.I don't know yet what the problem is, just letting you know that it exists. :)