Enzo Crance (Dec 01 2020 at 13:49): 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?
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).
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.
Enrico Tassi (Dec 01 2020 at 14:39):Elpi ( ) is a bit more expressive than Prolog, you may peek at the two tutorials linked from the main page.
Last updated: Apr 20 2024 at 01:41 UTC