Creating a Coq function in Coq-Elpi · Elpi users & devs

Stream: Elpi users & devs

Topic: Creating a Coq function in Coq-Elpi

Enzo Crance (Feb 08 2021 at 14:01):

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.

Enrico Tassi (Feb 08 2021 at 14:12):

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

Enrico Tassi (Feb 08 2021 at 14:23):

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)

Enzo Crance (Feb 08 2021 at 14:29):

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

Enzo Crance (Feb 08 2021 at 14:30):

Thank you very much for the pi explanations again! I'll have a look and try to make my way.

Enrico Tassi (Feb 08 2021 at 14:32):

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

Enrico Tassi (Feb 08 2021 at 14:42):

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: Apr 19 2024 at 13:02 UTC