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 ?
What you need is
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
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.
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: Feb 04 2023 at 01:03 UTC