[Beginner question] about binding with `pi`and `decl` · Elpi users & devs

Hi,
I have a question which is probably absurd. I'm trying to understand how binding works.
As an example, I give two examples of two functions, which are supposed to have the same specification.
Basically, I use an enumeration type blutwho has two inhabitants a and b. The functions mylistand myotherlist are partial: they scan a Coq term and produce a list of as and bs with the a standing for constant occurrences and b for lambdas.

Elpi Accumulate lp:{{

 kind blut type.
  type a blut.
  type b blut.

pred mylist i : term, o : (list blut).
mylist (global G) [a].
mylist (fun N Ty F) [b | R] :- !,
   mylist Ty R1, pi x\ decl x N Ty => mylist (F x) R2,
   std.append R1 R2 R.

pred myotherlist i : term, o : (list blut).
myotherlist (global G) [a].
myotherlist (fun N Ty F) [b | R] :- !,
   mylist Ty R1,  decl x N Ty, myotherlist (F x) R2,
   std.append R1 R2 R.
}}.

Elpi Query lp:{{
  mylist {{ fun (x: nat) => true }} R.
}}.

Fail Elpi Query lp:{{
  myotherlist {{ fun (x: nat) => true }} R.
}}.

The first function, mylist, works because I've used the query pi x\ decl x N Ty => mylist (F x) R2,. But what I don't understand is why I should declare a function with the pi binder. Afterall, I don't really use this function, I'm just interested in the body Fof (fun N Ty F) that I need applying to an argument. Instead, I tried to give another version of the function, called myotherlist which replaces the aforementioned query with decl x N Ty, myotherlist (F x) R2,. This does not work (cf. the end of the code). Yet, I was under the understanding that decl x N Ty would declare a local variable of type Ty whose name is N and which I can refer as x. But I guess the code fails because I didn't bind the metavariable x. Thus, my questions are the following:
1) why should the predicate decl only work with bound variable (with pi).
2) can I understand the pi binder as a kind of let ... in with the dots being handled with decl (thus, intuitively, pi is not a lambda

) ?
Because, in the end,

x the information that I am taking from the function, i.e. the phrase mylist (F x) R2 has a scope which is outside the scope of x (since mylist (F x) R2` ends up in the output of my function)

Enrico Tassi (Apr 12 2022 at 15:09):

I think it may help to rephrase your predicated as logical formulas, at least in the case of fun:

\forall R~R_1~R_2~N~Ty~F, mylist~Ty~R_1 \wedge (\forall x, decl~x~N~Ty \to mylist~(F~x)~R_2) \wedge append~R_1~R_2~R \to mylist (fun~N~Ty~F)~[b~|~R]

\forall R~R_1~R_2~N~Ty~F, mylist~Ty~R_1 \wedge (\forall x, decl~x~N~Ty \wedge mylist~(F~x)~R_2) \wedge append~R_1~R_2~R \to mylist (fun~N~Ty~F)~[b~|~R]

In the former case decl x N Ty is an extra assumption, while in the latter case it is an extra goal.
This is somehow documented here: https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_HOAS.html#the-context , see also the @pi-decl macro which helps not forgetting to assume decl whenever one uses a pi.

Operationally, it is pi x\ which generates a new variable x, and decl x N Ty => (a rule on the LHS of the implication =>) which adds some knowledge about it. decl is not special, you can put any rule on the LHS of =>, but by convention the Coq embedding of terms uses decl to represent typing context entries.

You should find a longer explanation of what I wrote here in the first two tutorials.

Pierre Vial (Apr 13 2022 at 13:41):

OK, thanks, I see a little better not! I hadn't completely understood the part about the tutorial which tackles def and def.
I guess there is some sort of dark magic which enables elpi to unify R2 in the first formula with a constraint pertaining to a variable, x, which has a limited scope (in the sense that it is not bound by a prenex quantifier).

Stream: Elpi users & devs

Topic: [Beginner question] about binding with `pi`and `decl`

Pierre Vial (Apr 12 2022 at 13:32):

Enrico Tassi (Apr 12 2022 at 15:09):

Pierre Vial (Apr 13 2022 at 13:41):