Stream: Elpi users & devs

Topic: Creating a Coq function in Coq-Elpi


view this post on Zulip Enzo Crance (Feb 08 2021 at 14:01):

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

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?

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.

view this post on Zulip Enrico Tassi (Feb 08 2021 at 14:12):

Enzo Crance said:

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

view this post on Zulip 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:

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

view this post on Zulip 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 }}).
}}.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC