Hi,

I would like to output a list of the form `[ X1 , .... , Xn ]`

where `n`

is a parameter and the `Xi`

are supposed to be placeholders for `term`

s.

What is wrong with this? (I get an unspecified error)

```
Elpi Command listX.
Elpi Accumulate lp:{{
pred listX i : int, o : list term.
listX (1 + k ) [X | L]:- listX k L.
listX 0 [].
}}.
Elpi Query lp:{{
listX 3 L. % ---> ERROR
}}.
```

PS: two very loosely related questions:

1) is there a way to print the `elpi`

type of an expression?

2) is there native pairs in `elpi`

or should we use list for that?

The code you are trying to write exists already: https://github.com/LPCIC/coq-elpi/blob/e4bf0b0b3e092b16c89b4e49d64523902fe24d13/elpi/coq-lib.elpi#L67

As well as the pair data type: https://github.com/LPCIC/coq-elpi/blob/e4bf0b0b3e092b16c89b4e49d64523902fe24d13/elpi-builtin.elpi#L228

Arithmetic evaluation happens via `is`

, you can write `N is M - 1`

, but you can't expect `N = 1 + M`

to compute. `1 + M`

is just syntax, `is`

gives it the meaning.

This is exactly what I needed. Thank you!

As a follow-up question, I would like to substitue these `k`

variables in a function which takes `k`

parameters, so do something like this:

```
Elpi Accumulate lp:{{
pred appk i : list term, i : term, o : term.
appk [ X0 | L ] (fun _ Ty Fu) (Fu' X0) :- appk L (Fu X0) (Fu' X0) .
appk [] T T.
}}.
Elpi Query lp:{{
appk [X0 , X1 ] {{fun (a b : nat) => a + b}} T.
}}.
```

However, I obtain this error:

```
Non deterministic pruning, delay to be implemented: t=
A4 ≪.X0≫_0, delta=0
```

What is wrong again?

I am not a master in Elpi internals but it seems to detect that `T`

depends on `X0`

after the call, yet the code does not reflect this.

First, I would suggest not to try to unify the output of `appk`

with a function applied to a unification variable. Instead of:

```
appk [X0|L] (fun _ Ty Fu) (Fu' X0) :-
appk L (Fu X0) (Fu' X0).
```

prefer the following:

```
appk [X0|L] (fun _ Ty Fu) (Fu' X0) :-
pi x\ appk L (Fu x) (Fu' x).
```

You create a universal constant `x`

that Elpi can easily abstract in `Fu'`

, whereas a unification variable can depend on other unification variables, etc. It usually works better. In my experience working with unification variables is tricky.

Then, I think the error would still be there, but it would come from the fact that `X0`

and `X1`

are unification variables in your query. For example, provided that you use the formulation with the universal constant, if you replace `X0`

and `X1`

with `{{ O }}`

, the code works.

```
Elpi Query lp:{{
appk [{{ 0 }}, {{ 0 }}] {{ fun (a b : nat) => a }} T.
}}.
```

```
Query assignments:
T = global (indc «O»)
```

OK, so if I take your line for `appk`

, I still have the exact same error with my initial query. But with your code and query, it works.

However, this solution won't work for what I'm endeavouring to do: I need some generic variables (which will have two occurrences in a proof term) and that I can bind afterwards.

Basically, I would like to be able to output something like: ` F X1 X2 ... Xn + G X1 ... Xn`

to be able to then build `pi x1\decl _ _ _ => .... pi xn\decl _ _ _ _ => F x1 ... xn`

(in fact, as you can expect, what I'm doing to do is more complicated than that and I need to tinker with the syntax of terms)

so from terms `f`

, `g`

and a number `n`

of arguments you want to create the binder `fun x1 ... xn => f x1 ... xn + g x1 ... xn`

?

something which is more complex than that, which plays with equalities, implication etc, but what I'm trying to understand how to manipulate variables (which will be bound) in a term that I build

I think there are a few idiomatic patterns to make code work, but I cannot really list them from memory, it's better with an example. idk how I could help more at this point. You can still ask other more experienced users. Good luck!

Thanks Enzo. I have new idea, I'll try to see if it works

You can also look for hd-beta in reducion.elpi (loaded by default) or coq.reduction.*

Last updated: Feb 05 2023 at 13:02 UTC