@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?

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).

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.

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

Last updated: Jun 06 2023 at 22:01 UTC