Stream: Elpi users & devs

Topic: Rewrite in Coq-Elpi


view this post on Zulip Enzo Crance (Feb 18 2021 at 19:33):

Is there a way to apply a rewrite lemma in elpi? If not, I have a backup solution to express it that requires to be able to beta-expand any term containing one or more occurrences of a value v into some P v. Is there a way to find that P in elpi?

view this post on Zulip Enrico Tassi (Feb 18 2021 at 20:03):

beta-expanding, as you call it, it's easy to do in elpi. It's a key component of HO unification, and elpi was meant for that. This piece of code from an (experimental) elaborator for Coq does that for a list of terms, not just one. https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-elaborator.elpi#L159 It's like "copy" but goes the other way.

There is a big question mark, that is "how do you compare a term with v" and what the code I wrote does is to use keyd-matching, a concept from ssreflect also use in the HO unification of matita. Depending on your user case you may want to change that.

view this post on Zulip Enrico Tassi (Feb 18 2021 at 20:04):

I hope you can follow that code, otherwise just ask.


Last updated: Feb 04 2023 at 02:03 UTC