Louise Dubois de Prisque (Apr 02 2022 at 16:01): Louise Dubois de Prisque (Apr 02 2022 at 16:01):Hello !
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.
Enrico Tassi (Apr 02 2022 at 18:20):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.
Louise Dubois de Prisque (Apr 03 2022 at 15:55):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 !
Enrico Tassi (Apr 04 2022 at 08:19):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]))
Enrico Tassi (Apr 04 2022 at 08:20):but if the context is not shuffled, then you can probably just pass the position in the context of the hyps you want.
Enrico Tassi (Apr 04 2022 at 08:22):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
Louise Dubois de Prisque (Apr 04 2022 at 11:59):Thanks a lot, this is what I needed, I will try to reimplement my tactic using the coq.ltac.set-goal-arguments utility
Last updated: Apr 18 2024 at 22:02 UTC