Stream: Elpi users & devs

Topic: Create new goal (assert in Elpi)


view this post on Zulip Louise Dubois de Prisque (Sep 01 2021 at 14:14):

Hello everyone ! I tried to do an elpi tactic similar to assert without using the ltac tactic.
My code is the following:

Elpi Tactic create_new_goal.
Elpi Accumulate lp:{{

  solve (goal Ctx _ _ _ [trm H] as G) GL :-

    GL = [seal G, seal G1],  G1 = goal Ctx _ H Ph [].

}}.
Elpi Typecheck.

But when I try to use the tactic I get this error : Not a goal seal (goal [] X22 (global (indt «True»)) X23 []) in evar X0 (global (indt «False»)) X1 /* suspended on X0, X1 */, I don't understand because I wrote seal, so if someone can help me to understand this, I would be gratful. I also tried something similar with msolve but I got the same problem. Thank you in advance for your help !

view this post on Zulip Enrico Tassi (Sep 01 2021 at 14:19):

Hi, thanks for trying Elpi! Indeed it would be nice to have an example of assert here: https://github.com/LPCIC/coq-elpi/tree/master/apps/eltac/theories
I'm currently in a call, but assert amounts to refining a beta redex. E.g. refine {{ (fun H : cut_formula => _) _ }} G GL should to the work.

view this post on Zulip Enrico Tassi (Sep 01 2021 at 14:20):

I'll try to write a working snippet later.

view this post on Zulip Enrico Tassi (Sep 01 2021 at 14:36):

Here something:

From elpi Require Import elpi.

Elpi Tactic create_new_goal.
Elpi Accumulate lp:{{

  solve (goal _ _ _ _ [trm H] as G) GL :-
    std.assert-ok! (coq.elaborate-ty-skeleton H _ H1) "cut formula illtyped",
    refine (app[(fun `new_hyp` H1 x\ G1_ x), G2_]) G GL,
    coq.say GL.

}}.
Elpi Typecheck.

Goal True.
elpi create_new_goal (False).

Note that creating goals by hand is hard, coq.ltac.collect-goals is there for that (and refine uses it).

view this post on Zulip Enrico Tassi (Sep 01 2021 at 14:37):

But maybe you can give me a bit more context, so that I can point you in the right direction.

view this post on Zulip Louise Dubois de Prisque (Sep 01 2021 at 17:55):

Thank you very much for your help, I will think about it and ask more precise question later


Last updated: Feb 04 2023 at 02:03 UTC