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 !

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.

I'll try to write a working snippet later.

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).

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

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

Last updated: Jun 23 2024 at 01:02 UTC