Enzo Crance (Jul 02 2021 at 09:16): Enzo Crance (Jul 02 2021 at 09:16):Hello. I am in trouble with an error when trying to apply a proof term. I am first generating a proof under a pi x, expressing it as P x, then there is this line
P' = (x'\ P (R x'))
where R is a simple Coq function expressed as a term -> term. P x contains some unification variables, and it looks like elpi considers them to depend on x (like X0 c0 X1 c0 etc), which can be justified: as we do not know what is there, we need to consider it to be able to depend on the variable, so that we do not lose generality.
Printing or applying this Coq term is OK, but when using P', now the proof depends on R x' and elpi refuses to apply it, and I don't know why. Here is the error (R is Z_to_int basically):
Flexible term outside pattern fragment:X2 (app [global (const «Z_to_int»), c2])
The unification variables that cause the error are the underscores in
@ssreflect.iffLR _ _ (* lemma talking about x (or R x') *)
I tried to minimise the error but could not reproduce it in a simple Elpi Query block.
Elpi Query lp:{{
pi x\
P x = {{ @ssreflect.iffLR _ _ (mylemma lp:x)}},
pi x'\
R x' = {{ Z_to_int lp:x' }},
P' = (x'\ P (R x')).
}}.
Here is the result (X0 and X1 do not depend on the variables anymore...):
P' = c0 \
app
[global (const «ssreflect.iffLR»), X0, X1,
app
[global (const «mylemma»),
app [global (const «Z_to_int»), c0]]]
Here is an extract from the proof before using R x' and after:
global (const «ssreflect.iffLR»), X0^1, X1^1, % ok
app [global (const «mylemma»), c0]
global (const «ssreflect.iffLR»),
X2 (app [global (const «Z_to_int»), c0]), % line causing the error
X3 (app [global (const «Z_to_int»), c0]),
app
[global (const «mylemma»),
app [global (const «Z_to_int»), c0]]
I also tried to create the Coq term by hand replacing the unification variables with underscores, it typechecks and the type actually is exactly what I expect to apply to the proof state, so the term is supposed to be well formed. Do you know where the error might come from?
Maybe these bugs come from the fun and forall binders in the proof where I do not give the types, assuming Coq is clever enough to guess them. In fact, I know Coq can guess them, but the elpi type system is different and what I am typing syntactically might be parsed into dependent unification variables, then when going back to Coq it causes the term to need more annotations to be well typed?
Enzo Crance (Jul 02 2021 at 09:21):I might not be clear enough for you to dive into the specificities, here is a more practical and general way to ask my question: how to deal with the following kind of error in elpi?
Flexible term outside pattern fragment
I am stuck because I do not know what the error really means.
Enrico Tassi (Jul 02 2021 at 09:24):OK, it will take some time but it's the good occasion to explain it.
First, beware that
pi x\
P x = {{ @ssreflect.iffLR _ _ (mylemma lp:x)}},
pi x'\
R x' = {{ Z_to_int lp:x' }},
does not read
(pi x\
P x = {{ @ssreflect.iffLR _ _ (mylemma lp:x)}}),
(pi x'\
R x' = {{ Z_to_int lp:x' }}),
as one may think. But this is not the problem here.
Enrico Tassi (Jul 02 2021 at 09:29):The "pattern fragment" identifies a class of higher order unification problems which are easy to solve, and which is at the base of \lambdaProlog and Elpi. Higher order means that the variable is in head position (it stands for a function) and pattern fragment that the variable is applied to distinct names. Eg, X c0 c1 c2 is in, while X c0 c0 is not, as well as X (app[global (const "f"), ...])
Enrico Tassi (Jul 02 2021 at 09:29):Elpi tolerates these terms but can only "pass them around".
Enrico Tassi (Jul 02 2021 at 09:30):If you trigger an unification, eg X c0 c0 = c0 or you pass them to Coq, you can get the error message.
Enrico Tassi (Jul 02 2021 at 09:31):If you look at the unification problem, you see that there are 2 solutions to it: X = (x\_\x) or X = (_\x\x), and Elpi does not known which one to pick.
Enrico Tassi (Jul 02 2021 at 09:36):Practically, it happens to substitute a name (like c0) with an arbitrary term and exit the fragment. According to my experience, one usually wants to pass these terms to Coq and there are ways to make the FFI accept the term. Two actually:
@holes! => coq.typecheck (X (app[...])) tells Elpi to purge the offending argument https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L209skeletons, eg coq.elaborate-skeleton which consider flexible terms as fresh holes (disregarding their arguments) Enzo Crance (Jul 02 2021 at 09:38):Thanks a lot for your explanation. So a solution is to give more details in my proof terms and avoid underscores in elpi. Another solution is to call elaborate-skeleton before trying to apply the term, so that it is fully typed before going back to Coq?
Enzo Crance (Jul 02 2021 at 09:39):Enrico Tassi said:
If you look at the unification problem, you see that there are 2 solutions to it:
X = (x\_\x)orX = (_\x\x), and Elpi does not known which one to pick.
But how come that Coq can infer these underscores? Was my intuition true? That elpi adds some complexity by making the holes depend on variables, and when going back to Coq it does not typecheck? I hope my question isn't trivial :sweat_smile: thanks again for your time
Enrico Tassi (Jul 02 2021 at 09:39):Yes, I would take the latter option. Note that if you are writing a tactic, refine does so for you. If you are writing a command, yes, call elaborate before passing the term to Coq.
Enrico Tassi (Jul 02 2021 at 09:40):Yes, but the problem is not the variables in scope. The problem is that you substituted some variables for some terms.
Enrico Tassi (Jul 02 2021 at 09:41):This is an operation which puts you out of this fragment.
Enrico Tassi (Jul 02 2021 at 09:44):Here P' = (x'\ P (R x')) you pass to P a term, namely app [global (const "Z_to_int"), x'
Enrico Tassi (Jul 02 2021 at 09:44):And the _ you wrote see the variable you are replacing with app [global (const "Z_to_int"), x'.
Enrico Tassi (Jul 02 2021 at 09:45):There are also other ways around the problem, but it really depends what you want to do.
Enzo Crance (Jul 02 2021 at 09:46):I am actually in a tactic using refine, but it still fails (the problematic unification variables are in CoqProof):
refine {{ lp:CoqProof (_ : lp:NewGoal) }} InitialGoal NewGoals
However, I added a coq.elaborate-skeleton pass before this line and it seems to work. I will perform further testing but it is working a bit more now. Thank you!
Enrico Tassi (Jul 02 2021 at 09:46):If you write prune X [] https://github.com/LPCIC/elpi/blob/master/src/builtin.elpi#L405 then X has nothing is scope, if you use such an X in place of {{ _ }} you would not get that problem, but in general Elpi cannot know which variables you want to be in scope.
Enrico Tassi (Jul 02 2021 at 09:47):which version of coq-elpi are you using?
Enrico Tassi (Jul 02 2021 at 09:47):I think it should work in 1.10
Enrico Tassi (Jul 02 2021 at 09:48):before that refine was a bit buggy
Enzo Crance (Jul 02 2021 at 09:49):I am using 1.9.7
Enrico Tassi (Jul 02 2021 at 09:51):In 1.10 I've cleaned up the tactic layer quite extensively
Enrico Tassi (Jul 02 2021 at 09:52):I'm also writing more tutorials, but I've not finished yet.
Enrico Tassi (Jul 02 2021 at 09:53):I recommend you try to use the most recent version, which is 1.11.0 I believe.
Enrico Tassi (Jul 02 2021 at 09:54):See https://github.com/LPCIC/coq-elpi/blob/master/Changelog.md if you have troubles porting your code (the type of solve changed)
Enrico Tassi (Jul 02 2021 at 09:56):I can help porting your code if you like, see https://github.com/math-comp/algebra-tactics/pull/2 for example.
Just tell me which branch should I port (it must compile)
Enzo Crance (Jul 02 2021 at 09:59):It is ok, I am just using one call to refine so I just had a few lines to change. Thank you. Indeed it works without the elaborate-skeleton call now.
Enzo Crance (Jul 02 2021 at 10:01):btw I could help write a user-focused tutorial but I am not sure I would be precise enough. I am at least going to present Coq-Elpi to my research team as well as possible.
Enrico Tassi (Jul 02 2021 at 10:06):If you write something, I'll be happy to prof fread it and tell you if something is "incorrect". I this it is a really good idea, I can write tutorials, but my perspective is too biased, it is hard to foresee the pitfalls.
Enrico Tassi (Jul 02 2021 at 10:06):You perspective is much more interesting than mine!
Last updated: Oct 13 2024 at 01:02 UTC