Michael Soegtrop (Jun 12 2020 at 12:33): Michael Soegtrop (Jun 12 2020 at 12:33):@Enrico Tassi : I have a question regarding elpi: I have quite a few custom simplification functions - similar to ring_simplify but more special purpose. I wonder if Elpi would be an appropriate way to write such tactics. Essentially they take a term and return a modified term and a proof that the original term and the modieifed term are equal.
Enrico Tassi (Jun 12 2020 at 12:52):It is definitely possible to use Elpi for that, but without knowing more it is hard to tell if it can be of added value. First, it is a tactic right? Second, are your terms ground or they contain evars? (trying to guess which parts of Elpi you would need). Maybe you can just point me to some code.
Michael Soegtrop (Jun 12 2020 at 13:40):The terms are largish ground terms. Currently I write this in Ltac2. Since these simplifications are rule based, a Prolog like interface might lead to more readable code. E.g. in Ltac2 I have separate functions for doing similar transformations on separate types and structural pattern matching and checking conditions is syntactically not very nice. I would hope that in Elpi these could be grouped more logically and also more easily extended for a specific use case - like adding one rule just for one specific case. In Ltac2 this doesn't work easily - I would have to insert a pattern in a match before the catch all. From a semantic point of view the backtracking in Ltac2 is reasonably close to Prolog. Another thing which is not so nice in Ltac2 is that it doesn't help much in getting the types correct. Of cause Ltac is a strictly typed language, but a Gallina term is a Gallina term in Ltac2, so it doesn't help much in writing functions which construct a Gallina term of a specific type.
I thought about writing these transformations in Gallina, but it is tricky to then simplify / compute this Gallina term to exactly the right level. I experimented with inserting opaqueness borders, evaluating down to the opaqueness borders and use Ltac2 just to remove these borders - one can't easily do this last step in Gallina since one wouldn't know where to stop evaluating such a function.
Unfortunately this is proprietary stuff, so I cannot share it, but I could create some simple examples.
Enrico Tassi (Jun 12 2020 at 13:50):Michael Soegtrop said:
Unfortunately this is proprietary stuff, so I cannot share it, but I could create some simple examples.
From your description it seems Elpi could help.
Logic programming is bizarre in many ways, but has one thing I consider a true miracle: code is organized in clauses, adding one makes sense both syntactically and semantically. FTR lambdaProlog gives you "scoped" assert/retract (they correspond to logical implication) and it is very handy: you can add clauses both at run time (via implication) and at "program assembly" time.
It would be nice if you could give me a simple "mockup" (a couple of simplication systems, one built on the other + some patches). I like to put in the coq-elpi webpage simple example so that people can get an idea of what can be done. If you give the mockup I can write the elpi code, and the you can base on it in your actual application.
Janno (Jun 12 2020 at 14:09):I'd also be interested in the examples. This seems like it could be an interesting use case for Mtac2 given that you are worried about typedness of the Gallina terms. Mtac2 tactics can also be made extensible through typeclasses (and canonical structures), hopefully helping with the grouping aspect.
Michael Soegtrop (Jun 12 2020 at 14:11):OK, I see if I can come up with something self contained.
One more question: how does Elpi handle dependent types? Say I have rules which get a term and produce a dependent type with a new term and a proof that this term is equal to the parameter term. Would Elpi prevent me from inserting rules which would result in badly typed terms?
Michael Soegtrop (Jun 12 2020 at 14:14):@Janno : interesting. It might be an interesting use case to test various ways to write such tactics. In Computer algebra systems simplification is a very important topic - and very different from simplification in Coq which is about convertible terms.
Enrico Tassi (Jun 12 2020 at 14:16):The language imposes disciplined use of binders and has a ML like type system. It does not understand the type system of Coq natively, so you have to do some more work (at worse you call the coq type checker).
If you have time, please also give an example of a "bad clause" you'd like the "framework" to detect a way or another.
Last updated: Oct 03 2023 at 20:01 UTC