Stream: Elpi users & devs

Topic: Recursive Elpi tactic, or predicate modifying the goal

Pierre Vial (Sep 21 2022 at 12:07):

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.

Enrico Tassi (Sep 21 2022 at 12:54):

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?

Pierre Vial (Sep 21 2022 at 13:45):

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?

Enrico Tassi (Sep 21 2022 at 14:00):

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

Enzo Crance (Sep 21 2022 at 14:01):

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

Enzo Crance (Sep 21 2022 at 14:01):

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

Pierre Vial (Sep 22 2022 at 14:04):

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?

Enrico Tassi (Sep 22 2022 at 14:10):

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.

Enrico Tassi (Sep 22 2022 at 14:14):

This generates a term let x1 : T1 := B1 in let x2 : T2 := B2 in ... in _ and calls refine on it

Enrico Tassi (Sep 22 2022 at 14:16):

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

Pierre Vial (Sep 22 2022 at 14:39):

Thanks !

Pierre Vial (Sep 23 2022 at 13:44):

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.

Enrico Tassi (Sep 23 2022 at 13:55):

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.

Pierre Vial (Sep 23 2022 at 14:02):

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

Enrico Tassi (Sep 23 2022 at 14:09):

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: Oct 13 2024 at 01:02 UTC