Good afternoon. I have a few other questions about Coq-Elpi.

- The first one deals with Coq knowledge. How can we search for typeclass instances in the context? Is there any predicate like the following:

```
X = ..., Y = ...,
coq.typeclass-instance-exists {{ MyClass lp:X lp:Y }}.
```

or can we obtain a similar result using `coq.elaborate-skeleton`

, building a goal that has a unification problem whose solution is this particular instance?

- The second one is about creating Coq terms. Say I have a function
`f : T1 -> ... -> Tn -> T`

. I also have functions`g1`

, ...,`gn`

of types`T1' -> T1`

, ...,`Tn' -> Tn`

. I would like to create the following function:

```
f' := fun (x1 : T1') ... (xn : Tn') => f (g1 x1) ... (gn xn)
```

I have read the part of the tutorial about creating Coq terms but I am struggling when trying to write the predicate for this. Let's say I first want to generate the header `fun x1 ... xn =>`

. Then I can write `{{ fun x => lp:X }}`

and recursively call the predicate on `X`

to create the rest of the header. This will eventually leave me with an incomplete term waiting for a body in order to be a well-typed function. At this point, I have no idea how to create the body because I did not remember the names of my variables. If I try to remember them, unfortunately, I cannot use `{{ x }}`

somewhere to put it in a list because I get the following error:

```
The reference x was not found in the current environment.
```

I know binders are hard and it looks like it is a strength of Coq-Elpi, so I must be completely missing something. Here is the example that gave the error:

```
Elpi Accumulate lp:{{
mkf F Gs [] Vars B :-
mkbody F Gs Vars B.
mkf F Gs [T|Ts] Vars {{ fun x : lp:T => lp:X }} :-
mkf F Gs Ts [{{ x }} | Vars] X.
mkbody F Vars (app [F | GVars]) :-
std.map2 Gs Vars apply GVars.
apply G Var {{ lp:G lp:Var }}.
}}.
```

I know the internal elpi value for `fun x : T => t`

is `T`

and an elpi function, so I think this would work and really give fresh names, even if `x`

exists somewhere in the context, but I need a way to fix the error about references. Maybe a sigma introducing a new unique variable? I have no clue how sigma and pi operators work, the only example I understood is the function typing rule in the STLC typechecker.

Enzo Crance said:

- The first one deals with Coq knowledge. How can we search for typeclass instances in the context? Is there any predicate like the following:
`X = ..., Y = ..., coq.typeclass-instance-exists {{ MyClass lp:X lp:Y }}.`

Ciao. It depends what you mean by context. There is this API: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L712 (and more in general stuff in `coq.TC.*`

).

Enzo Crance said:

`mkf F Gs [T|Ts] Vars {{ fun x : lp:T => lp:X }} :- mkf F Gs Ts [{{ x }} | Vars] X.`

The rule of thumb is that in order to recurse under a binder one has to use `pi`

and `=>`

.

Example:

```
mkf F Gs [T|Ts] Vars {{ fun y : lp:T => lp:(B y) }} :-
pi x\
decl x `x` T =>
mkf F Gs Ts [x| Vars] (B x).
```

I renamed `x`

to `y`

in the first line to stress that it's not the same `x`

at line 2. Remarks:

`B`

(which is an elpi unification variable) must see`y`

(which is a Coq variable). You can write`lp:{{ B {{ y }} }}`

, or the shorter`lp:(B y)`

(it's equivalent)- Now,
`pi x\`

"allocates" a fresh symbol for the rest of the clause,`x`

is a term of type`term`

, exactly as`{{ y }}`

in the first line `B x`

substitutes in the body (to be created later) the bound variable with`x`

- the
`decl symbol name type`

clause can be added to the program to that, later on, if you call Coq's API on a term containing`symbol`

it knows its type. There is a "macro" to ease your life, namely the last 3 lines can be replaced by

```
@pi-decl `myname` T x\ mkf F G Ts [x|Vars] (B x)
```

Thanks. I think I have a working example. Is the following code the right way to check if an instance exists?

```
Class Default (T : Type) := {
d : T
}.
Instance defnat : Default nat := { d := 0 }.
Elpi Accumulate lp:{{
inst-typ T (tc-instance I _) :-
coq.typecheck (global I) T ok.
}}.
Elpi Query lp:{{
global ClassRef = {{ Default }},
coq.TC.db-for ClassRef L,
std.exists L (inst-typ {{ Default nat }}).
}}.
```

Thank you very much for the `pi`

explanations again! I'll have a look and try to make my way.

Let me rephrase the clause, maybe it will clairfy

```
mkf F Gs [T|Ts] Vars R :-
R = fun `y` T (y\ B y),
pi x\
decl x `x` T =>
mkf F Gs Ts [x|Vars] (B x).
```

This is the essence of binder mobility: you have a binder in the data you are processing/building "fun `y`

T (y\ B y)" and in order to work on a subterm which lives under a binder ("y\" here) you postulare a fresh symbol "x", you put in your context some knowledge about "x" (like its type and its pretty printing string) and finally you substitute the bound variable with thew fresh symbol "(y\ B y) x" (which you can't write like that, but that is the idea).

Enzo Crance said:

I think I have a working example. Is the following code the right way to check if an instance exists?

Not bad!

The only minor problem I see is that `(global I)`

may have parameters... imagine something like `Instance deflist A : Default (list A) := { d := @nil A }.`

.

In that case you probably need to build `app [ global I | Args ]`

. One handy tool is https://github.com/LPCIC/coq-elpi/blob/master/elpi/coq-lib.elpi#L80, a bit above you also find `mk-n-holes`

and `count-prods`

which you may use to pad `global I`

with some `_`

.

FYI, you can use `coq.locate "Default" ClassRef`

, but your code is also OK as long as the type class is defined when elpi "compiles" the program.

Last updated: Jun 07 2023 at 00:01 UTC