Louise Dubois de Prisque (Feb 25 2022 at 15:52): Louise Dubois de Prisque (Feb 25 2022 at 15:52):Hello ! I tried to write an elpi function to find the context of a sealed-goal. Indeed, using the local context is one of the step for my main tactic which deals with several subgoals.
My first trial was to write this predicate:
pred context_seal_goal i: sealed-goal, o: goal-ctx.
context_seal_goal (nabla G) Ctx :- !, pi x\ context_seal_goal (G x) Ctx, coq.say (G x).
context_seal_goal (seal (goal Ctx _ _ _ _ as G)) Ctx :- coq.say Ctx.
context_seal_goal _ _ :- coq.say "this should not happen".
However, when I applied it on some example, the second rule is never encountered, and I don't understand why.
Could you help me please ?
Enrico Tassi (Feb 25 2022 at 17:33):What you need is coq.ltac.open :
pred open i:open-tactic, i:sealed-goal, o:list sealed-goal.
that lets you run an open-tactic (which puts his hands on a (goal Ctx ...) directly.
Your code does not work because the Ctx you allocate in the first rule and pass down does not see the x from pi x\ which can (and does) occur in G x. As a result the second rules fails to unify (Ctx is used twice).
This should clarify:
context_seal_goal (seal (goal Ctx1 _ _ _ _ as G)) Ctx2 :-
coq.say Ctx1, % contains x
coq.say Ctx2, % does not see x
std.spy(Ctx1 = Ctx2). % fails
The code of coq.ltac.open is a bit more involved than yours, but does essentially what your tried to write.
If you manage to craft a very simple test case for your code, then putting Elpi Trace "context_seal_goal". just before your elpi mycode. should print a (verbose, ugly...) trace, which will display the unification failure, among other things.
Louise Dubois de Prisque (Feb 25 2022 at 19:35):Thanks a lot for your answer! Indeed I needed to construct a predicate of the input type of coq.ltac.open from my initial one and it worked
Last updated: Oct 13 2024 at 01:02 UTC