Louise Dubois de Prisque (Sep 01 2021 at 14:14): 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 !
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.
Enrico Tassi (Sep 01 2021 at 14:20):I'll try to write a working snippet later.
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).
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.
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: Apr 20 2024 at 05:01 UTC