Hi,

Is it possible to define an `Elpi `

tactic (in a case where `Ltac`

cannot work since the tactic consumes `elpi`

objects, e.g. `elpi`

lists)? I didn't find anything pointing to this in the tutorials

(Probably a follow-up to #narrow/stream/253928-Elpi-users-.26-devs/topic/Recursive.20Predicate/near/290215538 )

Actually, I would also go with an effectful `pred`

which modifies the goal with `solve`

but some trials show me that it is probably not possible.

I'm sorry but I don't understand the question. Can you write a mock up of the code, or show a concrete use case?

For instance, let say I want to take a term `T`

whose type is an inductive `I`

, whose constructors are ` C_1`

, ...., `C_n`

and prove in the local context the equalities

`C_1 = C_1`

, ... , `C_n = C_n`

.

I guess I should start with something like this:

```
solve (goal _ _ _ _ [trm T] as G) GL :-
coq.typecheck T Ty ok,
(global (indt I) = Ty ; app [global (indt I) | _ ] = Ty),
coq.env.indt I _ _ P _ Ks _, ....
```

Now, I have `Ks`

, the list of the constructors (of type `list constructor`

).

But now, I would like to do a loop on `Ks`

which would look like this:

```
Ks = [ K | TKs], C = global (indc K),
coq.ltac.call "assert" [trm (app [@eq , _ , C , C]) ] G [seal G1 | GL], ... , coq.ltac.call "reflexivity" ....,
%%%% redo the loop on TKs until it is empty
```

Is there a way to to this?

I don't have many conbinators at the level of goals, anyway they are here:

https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-ltac.elpi#L54

if you std.map Ks to build a tactic (whose code is roughly what you wrote) then `thenl`

is probably what you need

IMO, doing this with a single call to Coq would be easier. `refine`

with a series of `let`

bindings that you forge in one traversal of your list of constructors

might be biased because I usually run from Ltac like it's the plague

Enzo Crance said:

IMO, doing this with a single call to Coq would be easier.

`refine`

with a series of`let`

bindings that you forge in one traversal of your list of constructors

Would you have a simple example of such a code?

untested pseudocode:

```
make-lets [] {{ _ }}.
make-lets [T|TS] {{ let x : lp:T := lp:B in lp:(R x) }} :-
B = {{ ... }},
@pi-def `x` T B x\
make-lets TS (R x).
solve (goal ... L as G) GS :- make-lets L P, refine G P GS.
```

This generates a term `let x1 : T1 := B1 in let x2 : T2 := B2 in ... in _`

and calls refine on it

So the trailing _ is the new goal, which should see all the x1 .. xn

Thanks !

How should I make a `tactic`

out of an `open-tactic`

? Doing this like that for instance, but it fails without a specific error message (so I suppose the types are good):

```
Ltac myassert x := assert x.
Elpi Query lp:{{
T = open (x\ y\ coq.ltac.call "myassert" [trm True] x y),
coq.ltac.thenl T SG L.
```

You can't run tactic code in a query without crafting a goal by hand.

Try to define a tactic, then start a goal, and then call the tactic.

ok, but is indeed `open (x\ y\ coq.ltac.call "myassert" [trm True] x y)`

a legit `tactic`

?

I don't have the code at hand, but probably yes (and you don't need the eta expansion).

Not sure you need to open if you begin with `solve`

, see https://github.com/LPCIC/coq-elpi/blob/master/examples/example_reflexive_tactic.v#L257

Last updated: Jun 25 2024 at 14:01 UTC