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: Jul 23 2024 at 19:02 UTC