Stream: MetaCoq

Topic: Boolean equality on template terms


view this post on Zulip Louise Dubois de Prisque (Dec 14 2023 at 09:13):

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 !

view this post on Zulip Théo Winterhalter (Dec 14 2023 at 09:17):

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?

view this post on Zulip Théo Winterhalter (Dec 14 2023 at 09:18):

There is also an instance of EqDec for term: https://github.com/MetaCoq/metacoq/blob/coq-8.16/template-coq/theories/ReflectAst.v#L60

view this post on Zulip Théo Winterhalter (Dec 14 2023 at 09:19):

The Reflect instance is built from it. But it should compute, so I'd say if it doesn't then it's a bug.

view this post on Zulip Louise Dubois de Prisque (Dec 14 2023 at 09:22):

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.

view this post on Zulip Matthieu Sozeau (Dec 15 2023 at 13:17):

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