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 like`T' = 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!

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.

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.

Sorry for all the questions!

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

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.

It could be a simple map from the whole `GRing.my_operation Zmodstuff`

expressions to my custom `int.add`

, `mul`

, ..., functions. Maybe I am over-thinking the problem.

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

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.

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.

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

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
```

You are welcome! Have a nice evening.

@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" ?

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~~topictitled "Custom reduction" ?

Done. (I think anyone can do this though)

Last updated: Nov 29 2023 at 06:01 UTC