Hello,
I use MetaCoq
to implement Coq plugins, and I sometimes need to compare two terms (from Metacoq.Template
), with a boolean equality.
The only solution I found was to translate the terms into PCUIC
one, and use eqb_term
from PCUICEqualityDec
.
This is not satisfying at all because this is the only place in my code where I need PCUIC
, which means I have PCUIC
as an opam
dependency and as you now compiling it takes time. I would like to depend only on template-coq
, and in my opinion that would make more sense.
I managed to define eqb_term
as Definition eqb_term := @MetaCoq.Utils.ReflectEq.eqb term reflect_term.
, but for some
reason this is not usable for computations. (I am not familiar with MathComp
and its Reflect
).
Do you know a way to work around this problem? Is there something obvious that I am missing ?
Thank you for your help !
You also have eq_term
in the Checker
module: https://github.com/MetaCoq/metacoq/blob/coq-8.16/template-coq/theories/Checker.v#L366
I'm not sure what you need from this function. Do you need also to know it's correct?
There is also an instance of EqDec
for term
: https://github.com/MetaCoq/metacoq/blob/coq-8.16/template-coq/theories/ReflectAst.v#L60
The Reflect
instance is built from it. But it should compute, so I'd say if it doesn't then it's a bug.
That's what I needed, thanks Théo :) I don't need to prove correctness, I use everything in a 'skeptical' way . I'll try this new function and if this time I don't encounter the problem I have with Reflect
, I'll let you know because indeed there might be a problem with Reflect
.
Reflect doesn’t compute usually because it embeds the proof IIRC, but we do need a computable variant of equality to run the safechecker and erasure inside Coq
Last updated: Oct 13 2024 at 01:02 UTC