i everybody,
In a project, I would like to clear the bodies (with Ltac's clearbody
) of the identifiers which are given in a list of lists of an encapsulating type.
Basically, I would like the two Fail
s below not to happen.
Inductive my_idents :=
one_id (s : ident ) : my_idents.
Ltac clearbody_id_list l :=
match eval hnf in l with
| [] => idtac
| ?ctor :: ?l0 => match eval hnf in ctor with
| one_id ?idn => let x := constr:(idn) in
let _ := match goal with _ => clearbody x end in clearbody_id_list l0
end
end.
Ltac clearbody_id_llist l :=
match eval hnf in l with
| [] => idtac
| ?l0 :: ?tl0 => clearbody_id_list l0 ; clearbody_id_llist tl0
end.
Goal forall (n1 n2 : nat) (b1 b2 : bool), False.
Proof.
intros.
pose [[ one_id "n1" ; one_id "b2"] ; [] ; [one_id "b1"]] as l.
pose [ one_id "n1" ; one_id "b2"] as l0.
Fail clearbody_id_list l0.
Fail clearbody_id_llist l.
Abort.
I guess that it partly does not work because of Ltac
evaluation order, and partly because, in the current code, I should convert ident
s into Ltac names (the code does not work either when I remove constr:
around x in the first tactic, but with a slightly different error).
How shoud I do?
I rewrote your stuff by taking out a clearbody_id_ctor
and it already is a problem.
From Coq Require Import List String.
Import ListNotations.
Open Scope string_scope.
Definition ident := string.
Inductive my_idents :=
| one_id (s : ident) : my_idents.
Ltac clearbody_id_ctor ctor :=
match eval hnf in ctor with
| one_id ?idn =>
let x := constr:(idn) in
match goal with _ => clearbody x end
end.
Ltac clearbody_id_list l :=
match eval hnf in l with
| [] => idtac
| ?ctor :: ?l0 =>
clearbody_id_ctor ctor ;
clearbody_id_list l0
end.
Ltac clearbody_id_llist l :=
match eval hnf in l with
| [] => idtac
| ?l0 :: ?tl0 => clearbody_id_list l0 ; clearbody_id_llist tl0
end.
Goal forall (n1 n2 : nat) (b1 b2 : bool), False.
Proof.
intros.
pose [[ one_id "n1" ; one_id "b2"] ; [] ; [one_id "b1"]] as l.
pose [ one_id "n1" ; one_id "b2"] as l0.
Fail clearbody_id_ctor (one_id "n1").
Fail clearbody_id_list l0.
Fail clearbody_id_llist l.
Abort.
Isn't it the case that the only problem is converting strings to Coq identifiers?
I tried something simpler I think which fails for a different reason:
From Coq Require Import List.
Import ListNotations.
Inductive my_idents :=
| one_id {A : Type} (a : A) : my_idents.
Ltac clearbody_id_ctor ctor :=
match eval hnf in ctor with
| one_id ?idn =>
clearbody idn
end.
Ltac clearbody_id_list l :=
match eval hnf in l with
| [] => idtac
| ?ctor :: ?l0 =>
clearbody_id_ctor ctor ;
clearbody_id_list l0
end.
Ltac clearbody_id_llist l :=
match eval hnf in l with
| [] => idtac
| ?l0 :: ?tl0 => clearbody_id_list l0 ; clearbody_id_llist tl0
end.
Goal forall (n1 n2 : nat) (b1 b2 : bool), False.
Proof.
intros.
pose [[ one_id n1 ; one_id b2] ; [] ; [one_id b1]] as l.
pose [ one_id n1 ; one_id b2] as l0.
Fail clearbody_id_ctor (one_id n1).
Fail clearbody_id_list l0.
Fail clearbody_id_llist l.
Abort.
But if you do this:
pose (n3 := 0).
clearbody_id_ctor (one_id n3).
it works.
Thanks a lot @Théo Winterhalter !
So, if I understand correctly, clearbody
takes its parameter as a Ltac
name, but there is not systematic way to have a Ltac
function from the Coq type string
to what would be the type of Ltac
names (I don't know how to call them), except, I guess, if I delve into OCaml
As a side remark, to give context, one_id
is MetaCoq
constructor for local variablestVar
Ah so you cannot use the trick I used.
There are ways using Ltac2 but I just know they exist.
there's this stuff https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/string_ident.v
Thanks @Gaëtan Gilbert
Actually, I've tried to cook up something by tinkering withintros_by_string
Ltac2 cleabody2 s := ltac1:(s |- clearbody s).
Ltac clearbody_id s := ltac2:(s1 |- let s := get_opt (Ltac1.to_constr s1) in
let ident := coq_string_to_ident s in
clearbody2 ident).
but it actuallys miserably fails. I don't understand how to fix that up with a $ , a ' or a &
You need to apply the ltac1 thunk in the clearbody2 case. Don't you get a no-unit warning somewhere?
if you print the type of clearbody2 you'll see there is an issue
Pierre-Marie Pédrot said:
if you print the type of clearbody2 you'll see there is an issue
Is there an equivalent of Check
for Ltac2
? Didn't find anything in the doc
Print Ltac2 foo.
should do the trick, although it also prints the tactic.
Ok, so I get :
clearbody2 : 'a -> Ltac1.t -> unit
(incidently, an r
was missing in my first definition of clearbody2
)
For the definition of clearbody_id
, I indeed get the warning The following expression should have type unit. [not-unit,ltac]
And last, for Fail clearbody_id k.
, I get the message
The command has indeed failed with message:
Unbound value clearbody_id
which is strange, since the definition of clearbody_id
was accepted.
The warning indicates that you haven't applied your function enough.
As you can see from the type, the first argument is not used.
Basically you have to apply your Ltac1 thunk to s in the first definition.
Huh, and how could I do this?
You write an application?
The syntax ltac1:(x |- foo)
binds x into foo
it's a closure, not a term that mentions some external x variable
ok, so basically, ltac:(x |- foo)
works like a fun
.
So now the second def fails:
Ltac2 clearbody2 s := ltac1:(s |- clearbody s) s.
Fail Ltac clearbody_id s := ltac2:(s |- let s2 := get_opt (Ltac1.to_constr s) in
let ident := coq_string_to_ident s2 in
clearbody2 ident) .
with the error message This expression has type ident but an expression was expected of type Ltac1.t
So, how is this fixable?
What's the intended content of s
in your Ltac1 definition?
A Coq term, an Ltac ident, something else?
Ltac2 clearbody2 s := ltac1:(s |- clearbody s) (Ltac1.of_ident s).
A Coq term of type string
So indeed @Gaëtan Gilbert solution is the way to go.
(you don't even have to define an intermediate Ltac2 def btw.)
Mmh, unfortunately, I can't work with Coq's latest version on my project for now, so of_ident
is yet unknown.
Pierre-Marie Pédrot said:
(you don't even have to define an intermediate Ltac2 def btw.)
Indeed, that was just intended to help decompose the functions
Yeah but in that case I'd have moved as much as possible the Ltac2 code to its own def and only write a trivial wrapper in Ltac1
Hum, apparently this thread has a "solution" here: https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/.60idtac.60.20and.20then.20.60clearbody.60on.20a.20list.20.28of.20lists.29.20of.20terms
Last updated: Oct 13 2024 at 01:02 UTC