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.

Paolo Giarrusso (Jul 18 2022 at 15:52):

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: Apr 20 2024 at 14:01 UTC