`idtac` and then `clearbody`on a list (of lists) of terms · Elpi users & devs

Hello,
I would like to clear the bodies (Ltac's clearbody) of local variables whose identifiers are given as a list (of lists) of a wrapper type, such as l1 and l0below:

Inductive my_idents :=
  one_id (s : ident ) : my_idents.


Elpi Command clear_body_list. (* ignore this command for now *)
Elpi Accumulate lp:{{
  main [trm L] :-
  coq.unify-eq L (app [ {{ @cons }}, X , T , L0 ]) ok,
  coq.ltac.call "idtac"  T, main [trm L0].
}}.
Elpi Typecheck.

Goal forall (n1 n2 : nat) (b1 b2 : bool), False.
Proof.
intros n1 n2 b1 b2.
pose [[ one_id "n1" ; one_id "b2"] ; [] ; [one_id "b1"]] as l1.
pose [ one_id "n1" ; one_id "b2"] as l0.
Fail Elpi clear_body_list [ one_id "n1" ; one_id "b2"].  (* ignore this line for now *)

I want to start modestly by just applying idtac and not clearbody , and that on simple lists of generic terms on not just on list of lists of inhabitants of one_id.

So I've written the (for now ill-named) command clear_body_list above, which fails without giving a specific error message.
Any tips on why it goes wrong ? Perhaps the recursive-call is ill-formed? I guess it is not use to have a specific case for dealing with empty lists?

Enrico Tassi (Jun 29 2022 at 14:40):

Something is off with your IDE, since I get a failure on Elpi Typecheck: "T has type term but is used with type (list argument)". Also you want to write a tactic and not a command.

From elpi Require Import elpi.

Elpi Tactic clear_body_list.
Elpi Accumulate lp:{{

  pred drop-body i:list argument, i:prop, o:prop.
  drop-body ToBeCleared (def V Name Ty _Bo) (decl V Name Ty) :- std.mem ToBeCleared (trm V), !.
  drop-body _ (decl _ _ _ as X) X.
  drop-body _ (def _ _ _ _ as X) X.

  msolve [nabla G] [nabla G1] :- pi x\ msolve [G x] [G1 x].
  msolve [seal  (goal Ctx _ T E ToBeCleared)] [seal (goal Ctx1 _ T E1 [])] :-
    std.map Ctx (drop-body ToBeCleared) Ctx1,
    @ltacfail! 0 => % this failure can be catch by ltac
      Ctx1 => % in the new context, do...
        std.assert-ok! (coq.typecheck-ty T _) "cannot clear since the goal does not typecheck in the new context",
    Ctx1 => std.assert-ok! (coq.typecheck E1 T) "should not happen", % E1 see all the proof variables (the pi x in the nabla case) and T is OK in Ctx1
    E = E1. % we make progress by saying that the old goal/evar is solved by the new one (which has the same type thanks to the line above)

}}.
Elpi Typecheck.

Tactic Notation "clear_body_list" hyp_list(l) := (* ltac1 will check that all arguments are names corresponding to existing proof variables *)
  elpi clear_body_list ltac_term_list:(l).

Lemma test1 : forall (n : nat) (b := n + 1) (r := b), nat.
Proof.
intros n b r.
clear_body_list b r.
exact b.
Show Proof.
Qed.

Enrico Tassi (Jun 29 2022 at 14:41):

And this other HACK is absolutely not in the spirit of Elpi, but is a fundamental brick of your approach (which I discourage):

From Coq Require Import String.
Open Scope string_scope.

Inductive my_idents :=
  one_id (s : string ) : my_idents.

Ltac myclearbody x := clearbody x.

Elpi Tactic string2term.
Elpi Accumulate lp:{{

  solve (goal Ctx _ _ _ [trm Str] as G) GL :- std.spy-do! [
    coq.term->string Str SQ,  rex.split "\"" SQ [S], % hack, there is no API to turn a Coq string into an Elpi string, other than the pretty printer
    coq.say "looking for" S,
    (std.mem Ctx (def X N _ _), coq.name->id N S), % hack, the name of context entries is a pretty printing hint, here we use it (via an unsound API, documented as such)
    coq.ltac.call "myclearbody" [trm X] G GL,
  ].

}}.
Elpi Typecheck.

Lemma test2 : forall (n : nat) (b := n + 1) (r := b), nat.
Proof.
intros n b r.
elpi string2term ("b").
exact b.
Show Proof.
Qed.

Enrico Tassi (Jun 29 2022 at 14:44):

In some sense Elpi tries hard to manage names for you, while here you reify names using Coq strings, and there is no decent API to link the two (since you should not use strings to denote bound variables in HOAS).

Enrico Tassi (Jun 29 2022 at 14:49):

Your code to traverse a Coq list is OK as far as I can tell, even if it lacks the case for nil. I did not run it: it does not type check.

Pierre Vial (Jun 29 2022 at 15:09):

Thanks a lot! I'll try to understand all that. It's perhaps that I'm using coq-elpi.1.13.8 and not 1.14.0 (all that on vscode)?

Enrico Tassi (Jun 29 2022 at 21:12):

Hum, I did my test on coq 8.16rc1 and coq-elpi master, but that should be the same on 1.14.0 on Coq 8.15.
About vscoq, I once had a bug (fixed now) which would not color errors in red, so maybe this is why you did not see the type error.

Enrico Tassi (Jun 29 2022 at 21:13):

BTW I did update the code above, making it interact better with ltac (see the @ltacfail! 0 option)

Stream: Elpi users & devs

Topic: `idtac` and then `clearbody`on a list (of lists) of terms

Pierre Vial (Jun 29 2022 at 13:53):