## Stream: Elpi users & devs

### Topic: Using `abstract` from Ltac1 in Elpi

#### Paolo Giarrusso (Jul 18 2022 at 09:37):

Does the coq-elpi -> Ltac1 bridge support `abstract`? In particular, in `Defined` blocks, `abstract` has side effects defining global constants, and those don't seem to work correctly — they produce axioms, but when used manually they produce proofs. (This is with coq-elpi 1.14.0).

Here are the (non-minimized) symptoms:

``````Ltac solve_finite_nodup := vm_decide.
Ltac solve_finite_total := case; vm_decide.
Ltac solve_finite Fields :=
refine (@Build_Finite _ _ Fields _ _);
[ abstract solve_finite_nodup
| abstract solve_finite_total ].

Variant t := A | B | C.
#[global] Instance: EqDecision t.
Proof. solve_decision. Defined.
Definition t_finite2 : Finite t.
solve_finite [A; B; C].
Defined.
(* new elpi command producing `t_finite` using `solve_finite [A; B; C].` *)
Print t_finite2.
Print t_finite.
Print t_finite2_subproof.
Print t_finite2_subproof0.
Print elpi_subproof.
Print elpi_subproof0.
(*
t_finite2 =
{|
enum := [A; B; C];
NoDup_enum := t_finite2_subproof;
elem_of_enum := t_finite2_subproof0
|}
: Finite t
t_finite =
{|
enum := [A; B; C];
NoDup_enum := elpi_subproof;
elem_of_enum := elpi_subproof0
|}
: Finite t
t_finite2_subproof =  (* ... defined correctly *)
t_finite2_subproof0 = (* ... defined correctly *)
*** [ elpi_subproof : NoDup [A; B; C] ]
*** [ elpi_subproof0 : ∀ x : t, x ∈ [A; B; C] ]

Arguments elpi_subproof0 x
*)
``````

#### Paolo Giarrusso (Jul 18 2022 at 09:42):

Forgot to add: it's likely I'm doing some naive mistake, but everything else _seems_ to work. Is there some way _I_ can screw up `abstract`?

#### Enrico Tassi (Jul 18 2022 at 11:30):

It is a bug, I did assume ltac1 tactics do not change the global environment...

#### Paolo Giarrusso (Jul 18 2022 at 13:18):

Thanks a lot for confirming despite my incomplete example :-)

#### Paolo Giarrusso (Jul 18 2022 at 13:19):

And I should say: I expected Coq-Elpi to be pretty good. In fact, getting started was even better, and Elpi was pretty forgiving :-)

#### Enrico Tassi (Jul 18 2022 at 15:41):

The bad news is that it is not easy to fix... I'll sleep on it.

Good luck!

#### Enrico Tassi (Jul 19 2022 at 09:31):

https://github.com/coq/coq/pull/16328 (it will work in 8.17, before it is too much work)

#### Paolo Giarrusso (Jul 19 2022 at 11:56):

Thanks! That's unfortunate, but it's easy enough to avoid `abstract` meanwhile thanks to elpi. As a sanity check, would the change let one reimplement `abstract` or pieces thereof in coq-elpi — say if you need `abstract` but aren't using ltac otherwise?

#### Paolo Giarrusso (Jul 22 2022 at 20:09):

Filed as https://github.com/LPCIC/coq-elpi/issues/376, just for tracking (= to mention in our TODOs)

Last updated: Feb 05 2023 at 14:02 UTC