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?

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.

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.

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"), ...])`

Elpi tolerates these terms but can only "pass them around".

If you trigger an unification, eg `X c0 c0 = c0`

or you pass them to Coq, you can get the error message.

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.

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#L209- use any API which talkes
`skeletons`

, eg`coq.elaborate-skeleton`

which consider flexible terms as fresh holes (disregarding their arguments)

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?

Enrico Tassi said:

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.

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

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.

Yes, but the problem is not the variables in scope. The problem is that you substituted some variables for some terms.

This is an operation which puts you out of this fragment.

Here `P' = (x'\ P (R x'))`

you pass to `P`

a term, namely `app [global (const "Z_to_int"), x'`

And the `_`

you wrote see the variable you are replacing with `app [global (const "Z_to_int"), x'`

.

There are also other ways around the problem, but it really depends what you want to do.

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!

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.

which version of coq-elpi are you using?

I think it should work in 1.10

before that `refine`

was a bit buggy

I am using 1.9.7

In 1.10 I've cleaned up the tactic layer quite extensively

I'm also writing more tutorials, but I've not finished yet.

I recommend you try to use the most recent version, which is 1.11.0 I believe.

See https://github.com/LPCIC/coq-elpi/blob/master/Changelog.md if you have troubles porting your code (the type of `solve`

changed)

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)

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.

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.

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.

You perspective is much more interesting than mine!

Last updated: Feb 04 2023 at 02:03 UTC