Stream: Elpi users & devs

Topic: Find a hypothesis in a sealed-goal


view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Feb 25 2022 at 17:38):

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.

view this post on Zulip 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: Feb 04 2023 at 01:03 UTC