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 `blut`

who has two inhabitants `a`

and `b`

. The functions `mylist`

and `myotherlist`

are partial: they scan a Coq term and produce a list of `a`

s and `b`

s 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 `F`

of `(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)

Thanks for reading :)

Pierre

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]$

v.s.

$\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.

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).

Last updated: Apr 21 2024 at 01:02 UTC