Stream: Elpi users & devs

Topic: Outputting a list of variables


view this post on Zulip Pierre Vial (Sep 11 2022 at 15:51):

Hi,
I would like to output a list of the form [ X1 , .... , Xn ] where n is a parameter and the Xi are supposed to be placeholders for terms.
What is wrong with this? (I get an unspecified error)

Elpi Command listX.

Elpi Accumulate lp:{{
  pred listX i : int, o : list term.
    listX (1 + k ) [X | L]:-  listX k L.
    listX 0 [].
}}.

Elpi Query lp:{{
    listX 3 L.   % ---> ERROR
}}.

PS: two very loosely related questions:
1) is there a way to print the elpi type of an expression?
2) is there native pairs in elpi or should we use list for that?

view this post on Zulip Enrico Tassi (Sep 11 2022 at 19:24):

The code you are trying to write exists already: https://github.com/LPCIC/coq-elpi/blob/e4bf0b0b3e092b16c89b4e49d64523902fe24d13/elpi/coq-lib.elpi#L67
As well as the pair data type: https://github.com/LPCIC/coq-elpi/blob/e4bf0b0b3e092b16c89b4e49d64523902fe24d13/elpi-builtin.elpi#L228

view this post on Zulip Enrico Tassi (Sep 11 2022 at 20:25):

Arithmetic evaluation happens via is, you can write N is M - 1, but you can't expect N = 1 + M to compute. 1 + M is just syntax, is gives it the meaning.

view this post on Zulip Pierre Vial (Sep 12 2022 at 09:44):

This is exactly what I needed. Thank you!

view this post on Zulip Pierre Vial (Sep 12 2022 at 11:25):

As a follow-up question, I would like to substitue these k variables in a function which takes k parameters, so do something like this:

Elpi Accumulate lp:{{
pred appk i : list term, i : term, o : term.
    appk [ X0 | L ] (fun _ Ty Fu) (Fu' X0) :- appk L (Fu X0) (Fu' X0) .
    appk [] T T.
}}.

Elpi Query lp:{{
  appk [X0 , X1 ] {{fun (a b : nat) => a + b}} T.
}}.

However, I obtain this error:
Non deterministic pruning, delay to be implemented: t= A4 ≪.X0≫_0, delta=0

What is wrong again?

view this post on Zulip Enzo Crance (Sep 12 2022 at 11:41):

I am not a master in Elpi internals but it seems to detect that T depends on X0 after the call, yet the code does not reflect this.

First, I would suggest not to try to unify the output of appk with a function applied to a unification variable. Instead of:

appk [X0|L] (fun _ Ty Fu) (Fu' X0) :-
  appk L (Fu X0) (Fu' X0).

prefer the following:

appk [X0|L] (fun _ Ty Fu) (Fu' X0) :-
  pi x\ appk L (Fu x) (Fu' x).

You create a universal constant x that Elpi can easily abstract in Fu', whereas a unification variable can depend on other unification variables, etc. It usually works better. In my experience working with unification variables is tricky.

Then, I think the error would still be there, but it would come from the fact that X0 and X1 are unification variables in your query. For example, provided that you use the formulation with the universal constant, if you replace X0 and X1 with {{ O }}, the code works.

Elpi Query lp:{{
  appk [{{ 0 }}, {{ 0 }}] {{ fun (a b : nat) => a }} T.
}}.
Query assignments:
  T = global (indc «O»)

view this post on Zulip Pierre Vial (Sep 12 2022 at 11:53):

OK, so if I take your line for appk, I still have the exact same error with my initial query. But with your code and query, it works.

However, this solution won't work for what I'm endeavouring to do: I need some generic variables (which will have two occurrences in a proof term) and that I can bind afterwards.
Basically, I would like to be able to output something like: F X1 X2 ... Xn + G X1 ... Xn to be able to then build pi x1\decl _ _ _ => .... pi xn\decl _ _ _ _ => F x1 ... xn (in fact, as you can expect, what I'm doing to do is more complicated than that and I need to tinker with the syntax of terms)

view this post on Zulip Enzo Crance (Sep 12 2022 at 12:10):

so from terms f, g and a number n of arguments you want to create the binder fun x1 ... xn => f x1 ... xn + g x1 ... xn?

view this post on Zulip Pierre Vial (Sep 12 2022 at 12:16):

something which is more complex than that, which plays with equalities, implication etc, but what I'm trying to understand how to manipulate variables (which will be bound) in a term that I build

view this post on Zulip Enzo Crance (Sep 12 2022 at 12:21):

I think there are a few idiomatic patterns to make code work, but I cannot really list them from memory, it's better with an example. idk how I could help more at this point. You can still ask other more experienced users. Good luck!

view this post on Zulip Pierre Vial (Sep 12 2022 at 13:26):

Thanks Enzo. I have new idea, I'll try to see if it works

view this post on Zulip Enrico Tassi (Sep 12 2022 at 13:29):

You can also look for hd-beta in reducion.elpi (loaded by default) or coq.reduction.*


Last updated: Feb 05 2023 at 13:02 UTC