Stream: Elpi users & devs

Topic: Elpi goal rewriting


view this post on Zulip Enzo Crance (Dec 01 2020 at 13:49):

@Enrico Tassi so I didn't understand everything in what you submitted as a POC for rewriting goals. I learnt Prolog a long time ago but have never used it since then, even less with lambda-calculus inside it. My first question is, does Elpi make proved rewritings on the goals, or is it uncertified? In that last case, I guess Coq generates a G' -> G cut in order to keep the proof logic correct. Am I right?

view this post on Zulip Enrico Tassi (Dec 01 2020 at 14:36):

Yes, the rewriting I do is not certified. You can either leave it to the user, or improve zify/contract to also generate a proof term (or a proof trace to be later turn into a proper term).

view this post on Zulip Enrico Tassi (Dec 01 2020 at 14:38):

The suffices tactic does that for you, the code I wrote just rewrites a term to another one in two steps, first pushing stuff to Z (and inserting a coercion to the old type) then removing the coercions when they cancel out. Maybe this design is silly, maybe not. It has the advantage to hopping between well type terms.

view this post on Zulip Enrico Tassi (Dec 01 2020 at 14:39):

Elpi ( λProlog\lambda Prolog) is a bit more expressive than Prolog, you may peek at the two tutorials linked from the main page.


Last updated: Feb 04 2023 at 01:03 UTC