I implemented a coq Elpi tactic which scans the proof context of a given goal. In particular, it collects information, such as particular variables in the context and uses them.
Suppose for instance that in elpi, the proof context has a variable
c0. The problem is that my tactic asserts and proves new hypothesis, and uses
c0. So it generates a new goal with a new hypothesis, and unfortunately all the variables are renamed. Then,
c0 becomes, say,
c4 in the new context. This leaded me to scan the proof context again, because
c0 does not exist anymore, and then do unnecessary redundant computations.
Is there any way to avoid this problem? Indeed, the new goal is only the previous one with a new hypothesis, so I guess the other context variables could have remained the same.
If you could share the code it would be much simpler for me to give you an advice. If you can't I'll try anyway. Can you share it? A link would suffice.
The link is here : https://github.com/louiseddp/sniper/blob/elpi_utilities/instantiate.v#L10. I have to make several calls to
find_instantiated_params_in_list because the parameters in my context are renamed every time I assert a new hypothesis. If it is not clear I can try to show you a minimal example to clarify my point. Thank you !
Thanks, I'm not sure I'll manage to look into it today, but I will ASAP. One way, not the most efficient one, is to say
coq.ltac.set-goal-arguments [trm c0] CurrentGoal NewSealedGoal NewSealedGoalWithArguments so that the new goal looks like
(nabla ... (goal _ _ _ _ [trm c4]))
but if the context is not shuffled, then you can probably just pass the position in the context of the hyps you want.
See also: https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_tactic.html#setting-arguments-for-a-tactic and tell me if it is not clear
Thanks a lot, this is what I needed, I will try to reimplement my tactic using the
Last updated: Feb 05 2023 at 13:02 UTC