## Stream: Elpi users & devs

### Topic: Elpi goal rewriting

#### 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 ( $\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