Stream: Elpi users & devs

Topic: Custom reduction

Enzo Crance (Jan 25 2021 at 17:26):

Thanks for your answer. Is there any way to trigger specific kinds of reduction in Coq-Elpi? I am thinking about things such as eval beta iota delta in ... in Ltac1, giving power to allow or disallow some kinds of reduction.

Say you have the 2 following structures.

Structure MyStruct1 : Type := mkS1 {
  field1 : nat -> nat -> nat
}.

Structure MyStruct2 : Type := mkS2 {
  field2 : MyStruct1
}.

Now if we hide Nat.add behind 2 layers of structures:

Definition s1 := mkS1 Nat.add.
Definition s2 := mkS2 s1.

Is there a way to reduce a term containing projections on these structures to get back Nat.add without Coq unfolding further, like the following:

Elpi Query lp:{{ T = {{ field1 (field2 s2) }}, coq.reduction.lazy.whd_all T T'. }}.

Looking for something likeT' = Nat.add, getting:

T' = fix `add` 0
 (prod `n` (global (indt «nat»)) c0 \
   prod `m` (global (indt «nat»)) c1 \ global (indt «nat»)) c0 \
 fun `n` (global (indt «nat»)) c1 \
  fun `m` (global (indt «nat»)) c2 \
   match c1 (fun `n` (global (indt «nat»)) c3 \ global (indt «nat»))
    [c2,
     (fun `p` (global (indt «nat»)) c3 \
       app [global (indc «S»), app [c0, c3, c2]])]

I guess the lazy reduction still uses delta reduction which unfolds definitions, if I am right. Anyway delta reduction is needed because of the definitions of s1 and s2, but maybe there is a way to trigger this type of reductions one by one until getting Nat.add, whereas the API seems to expose cbv and lazy which are both too "strong" for my needs. Sorry for all the questions!

Enrico Tassi (Jan 25 2021 at 17:47):

Currently all reduction functions are too strong for you ("all" stands for all reductions being active).
I'm OK adding more control, along the lines of eval lazy [-foo] .... I may have the time on Wednesday (but then you would need to install the .dev version of coq-elpi).

But I'd also like to know what you are doing exactly, since there are maybe other ways to skin the cat.
Do you really need efficiency? There is an implementation of whd in elpi/elpi-reduction.elpi which you may call, or use as a starting point to develop your own reduction strategy.

Enrico Tassi (Jan 25 2021 at 17:52):

If what you need is control and experimentation, then I would suggest at least prototyping your reduction in elpi. If you go this way, and you copy the code in you file, since the original code is already loaded, I suggest you either rename all predicates, or put you local copy inside a namespace myreduction { ... } (there is some documentation in ELPI.md) otherwise you risk to mix your copy with the original code.

Enrico Tassi (Jan 25 2021 at 17:59):

Sorry for all the questions!

Don't be, this is what this stream is for! Also, the doc is, hem, .... not there, so...

Enzo Crance (Jan 25 2021 at 18:07):

I'd like to change the generic ring operations like GRing.add into their counterparts in the underlying ring type, given in the structure that is the first parameter of these projections — addition on int for example. But I want to be able to recognise this is the addition on int, not some random int -> int -> int function. Thus I think keeping it folded under its name would be a simple way to go.
Moreover, I need to be able (me or the user) to add more structure fields / coercions like this to my tool in the future, so this must not be specific to rings.

Enzo Crance (Jan 25 2021 at 18:09):

It could be a simple map from the whole GRing.my_operation Zmodstuffexpressions to my custom int.add, mul, ..., functions. Maybe I am over-thinking the problem.

Enrico Tassi (Jan 25 2021 at 18:15):

Maybe then the simplest thing is to start from the copy function (in coq-lib.elpi), either by copying/renaming it and playing with it, or by "patching" it as I did in the CUDW talk (or in this more involved example https://github.com/LPCIC/coq-elpi/blob/master/examples/example_record_expansion.v).

Enrico Tassi (Jan 25 2021 at 18:18):

If you add in front of copy a rule like

copy {{ GRing.add int_RingType }} {{ Int.add }} :- !.

then it should do what you want, roughly.

Enrico Tassi (Jan 25 2021 at 18:19):

you can easily add more like this one, or make it more parametric and extract the operation out of int_RingType, but maybe this is what you were trying to do by calling reduction.

Enzo Crance (Jan 25 2021 at 18:22):

I'll look more deeply into this tomorrow. Thank you very much for your suggestions!

Enrico Tassi (Jan 25 2021 at 18:22):

if so you can try something along these lines

copy {{ GRing.add lp:X }} Y :- !,
  whd X [] K Args, std.nth 3 Args Y. %assuming the operation is in the 3rd field

Enrico Tassi (Jan 25 2021 at 18:23):

You are welcome! Have a nice evening.

Enrico Tassi (Jan 25 2021 at 19:08):

@Cyril Cohen would you mind separating messages starting from https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users.20.26.20devs/topic/Typing.20in.20coq-elpi/near/223931363 into a new stream titled "Custom reduction" ?

Cyril Cohen (Jan 25 2021 at 19:16):

Enrico Tassi said:

Cyril Cohen would you mind separating messages starting from https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users.20.26.20devs/topic/Typing.20in.20coq-elpi/near/223931363 into a new stream topic titled "Custom reduction" ?

Done. (I think anyone can do this though)

Last updated: Oct 13 2024 at 01:02 UTC