Luko van der Maas (Sep 25 2023 at 11:33): Luko van der Maas (Sep 25 2023 at 11:33):I am trying to make a tactic that calls refine several times on a goal and its subgoals. I got it to work, however it is renaming the variables. I have made a small tactic that reproduces the issue:
Elpi Tactic repro.
Elpi Accumulate lp:{{
solve (goal _Ctx _Trigger Type _Proof [] as G) GL :-
@no-tc! => refine {{ id _ }} G [G2],
coq.ltac.open (refine {{ id _ }}) G2 GL.
}}.
Elpi Typecheck.
Lemma foo (P : Prop) :
P -> P.
Proof.
elpi repro.
Show Proof.
This is the state after I run the above code
elpi_ctx_entry_1_: Prop
1/1
elpi_ctx_entry_1_ → elpi_ctx_entry_1_
And this is the proof:
(λ P : Prop, id (id ?elpi_evar@{elpi_ctx_entry_1_:=P}))
Does anyone have a solution?
Enrico Tassi (Sep 25 2023 at 11:46):The cause is that the solve entry point already loads a context, the second coq.ltac.open loads the (same) context again and I think this triggers a renaming.
You can do this:
Elpi Tactic repro.
Elpi Accumulate lp:{{
msolve [G] GL :-
@no-tc! => coq.ltac.open (refine {{ id _ }}) G [G2],
@no-tc! => coq.ltac.open (refine {{ id _ }}) G2 GL.
}}.
Elpi Typecheck.
In some sense, if you want to chain tactics, I think your main data type should be a sealed-goal. Ltac-like combinators work at this level, see elpi-ltac.elpi file.
Enrico Tassi (Sep 25 2023 at 11:47):In a way, the previous code was "nesting" the two coq.ltac.open, which is not a problem (the variables are made distinct) but the conversion from/to Coq is not smart enough to see one does not need a rename (on the Coq side).
Enrico Tassi (Sep 25 2023 at 11:48):I hope this works on you actual example.
Luko van der Maas (Sep 25 2023 at 11:59):Yes that's it, thank you very much.
Luko van der Maas (Sep 25 2023 at 12:00):I have one more question about this. Say I want to match on the type of the goal, for example if the type is a conjunction. Is it possible to do that in the msolve. Or should I do that inside the first coq.ltac.open?
Last updated: Oct 13 2024 at 01:02 UTC