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.

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 `coq.ltac.set-goal-arguments`

utility

Last updated: Jun 20 2024 at 11:02 UTC