[This is a follow-up of #narrow/stream/237977-Coq-users/topic/clearbody.20of.20a.20list.20of.20lists.20of.20identifiers ]

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 `l0`

below:

```
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?

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.

Here your multi clear body written in the spirit of Elpi

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

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

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

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.

Enrico Tassi said:

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.

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`

)?

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.

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

option)

I'm adding this example to the coq-elpi repository, here the commit: https://github.com/LPCIC/coq-elpi/commit/8928541b8e4473eb359873b6f040a53a964d8e7d

Last updated: Jun 25 2024 at 14:01 UTC