Enzo Crance (Dec 03 2021 at 18:40): Enzo Crance (Dec 03 2021 at 18:40):Hello. I would like to harness proofs using Elpi, that were made with the universe polymorphism option enabled, but when calling a tactic I get a "not yet implemented" error. What would it take to add this kind of feature to Coq-Elpi?
I will try to see if I can bypass this, but I am afraid it is likely to be a crucial point in the proofs I am using (univalent parametricity). I am willing to help if you don't have time to implement such a feature. I would just probably need an introduction to the Elpi internals beforehand.
Thanks in advance. Have a nice week-end.
Enrico Tassi (Dec 04 2021 at 06:55):Help is surely welcome. I have a PR to be refined. Maybe we can chat via visio next week?
Jasper Haag (Mar 24 2022 at 16:28):I have a related(?) issue so I'm reviving this thread; I'm happy to move to a new thread as well.
We have infrastructure for generating "hints" that can later be registered and utilized by our internal proof automation, and I would like to be able to execute this "hint" generation and registration within elpi. Unfortunately this infrastructure utilizes Set Universe Polymorphism/Set Polymorphic Inductive Cumulativity, and this results in terms containing universes. Based on the error message, it seems as if using coq.ltac.call to invoke the tactic succeeds in generating this (universe-containing) term - at which point the injection of the Coq-constr back into elpi fails; the constr2lp case for C.const calls check_univ_inst, which itself checks Univ.Instance.is_empty.
Generating and registering these "hint" terms is extremely important for our elpi use-case. Do you have a status update regarding support for this functionality (or a link to the relevant PR)? What blockers do you see w.r.t my particular use case?
Ali Caglayan (Mar 24 2022 at 19:49):Here is a relevant PR: https://github.com/LPCIC/coq-elpi/pull/315
Enrico Tassi (Mar 24 2022 at 20:11):Thanks Ali, yes we are working on it. I'll detail better the plan so that you can tell me which features are more relevant to you.
Enrico Tassi (Mar 24 2022 at 20:13):How to do it is now clear, but which feature to implement first is open. With that branch you can probably alreary read from coq a upoly term, but not write it for example.
Jasper Haag (Mar 25 2022 at 13:18):Wonderful! Thank you for working on this :~) I will take a look at the PR and comment regarding features which seem relevant to our use case (@Janno do you mind also taking a look?).
Fwiw, Janno was able to find a workaround which seems to be sufficient for the near-term use-cases we have for elpi, so luckily we are not immediately blocked on this feature. However, we certainly prefer an approach in which universes are handled in a principled way within elpi itself!
James Wood (May 04 2022 at 16:22):Just to make sure I'm not missing something: is the current (pre-PR) status of coq-elpi that it's incapable of dealing with any terms involving universe polymorphism? Or is there some workaround?
Enrico Tassi (May 05 2022 at 07:16):Not that I'm aware of, there is no work around. I count one more user interested in the feature. It happens both @Enzo Crance and mayself had to focus on other things, so https://github.com/LPCIC/coq-elpi/pull/315 did not make progress. Still you can already read a polymorphic term from the environment, but not write one to, with that PR, see the very simple example here: https://github.com/LPCIC/coq-elpi/pull/315/files#diff-913332ff5affe04bc3a3a00beb38b7164761f2f35c4f21fc11c17ec531c9ec2d
The current plan is to go back to work on this feature soonish, possibly with a sprint (in person) in June. Hope it helps.
Last updated: Jun 06 2023 at 23:01 UTC