Hello. I am trying to transform a pair of elpi values (a Coq term and a list of elpi functions) into a Coq function whose body applies the term to the elpi functions called on the bound variables. Starting from this:

```
G : term
[F1, ..., Fn] : list (term -> term)
```

I would like to make this:

```
fun x1 ... xn => lp:{{ app [G, F1 x1, ..., Fn xn] }}
```

I have been struggling for a while with the `pi`

operator once again, but have not managed to program it properly. Is there a standard way to do this? Thanks.

```
From elpi Require Import elpi.
Elpi Command test.
Elpi Accumulate lp:{{
pred loop i:list (term -> term), i:list term, i:term, o:term.
loop [] ArgsRev Head T :- std.rev ArgsRev Args, coq.mk-app Head Args T.
loop [F|Fs] ArgsRev Head (fun Label {{nat}} x\ Bo x) :-
coq.name-suffix `a` {std.length ArgsRev} Label, % not really needed
pi a\ % we need to move under x to build Bo, so we postulate a symbol a
loop Fs [F a|ArgsRev] % and we pass a to F
Head (Bo a). % and plays the role of x inside Bo
main _ :-
loop
[ (x\app[{{S}},x]) , (x\app[{{plus}},{{2}},x]) ] % These are the F1 ... Fn
[] % initial value of the accumulator ArgsRev
{{mult}} % this is G
T,
coq.say T.
}}.
Elpi test.
```

prints

```
fun `a0` (global (indt «nat»)) c0 \
fun `a1` (global (indt «nat»)) c1 \
app
[global (const «Nat.mul»), app [global (indc «S»), c0],
app [global (const «Nat.add»), ... , c1]]
```

This is a quite recurrent pattern, while you recurse, you apply the variable introduced by `pi`

to some argument.

Sorry, I don't have much time to explain further.

Enrico Tassi said:

This is a quite recurrent pattern, while you recurse, you apply the variable introduced by

`pi`

to some argument.

Sorry, I don't have much time to explain further.

Great. There is no elpi notion in your code that I do have never encountered before, so I will read it in detail and I think I will understand it. Thank you very much!

This one also works, but is less efficient, since `coq.mk-app`

has to append `[F a]`

at the end of `T`

, but if it is not a bottleneck, then this code is simpler.

```
pred loop i:list (term -> term), i:term, o:term.
loop [] T T.
loop [F|Fs] T (fun `a` {{nat}} x\ Bo x) :-
pi a\
loop Fs {coq.mk-app T [F a]} (Bo a).
```

Last updated: Jun 06 2023 at 22:01 UTC