Pierre Vial (Jun 27 2022 at 12:53): Pierre Vial (Jun 27 2022 at 12:53):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 Fails 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 idents 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?
Théo Winterhalter (Jun 27 2022 at 18:59):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.
Pierre Vial (Jun 27 2022 at 19:39):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
Théo Winterhalter (Jun 27 2022 at 19:41):Ah so you cannot use the trick I used.
There are ways using Ltac2 but I just know they exist.
Gaëtan Gilbert (Jun 27 2022 at 20:07):there's this stuff https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/string_ident.v
Pierre Vial (Jun 28 2022 at 08:49):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 &
Pierre-Marie Pédrot (Jun 28 2022 at 09:07):You need to apply the ltac1 thunk in the clearbody2 case. Don't you get a no-unit warning somewhere?
Pierre-Marie Pédrot (Jun 28 2022 at 09:07):if you print the type of clearbody2 you'll see there is an issue
Pierre Vial (Jun 28 2022 at 09:23):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
Pierre-Marie Pédrot (Jun 28 2022 at 09:24):Print Ltac2 foo. should do the trick, although it also prints the tactic.
Pierre Vial (Jun 28 2022 at 09:31):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.
Pierre-Marie Pédrot (Jun 28 2022 at 09:32):The warning indicates that you haven't applied your function enough.
Pierre-Marie Pédrot (Jun 28 2022 at 09:32):As you can see from the type, the first argument is not used.
Pierre-Marie Pédrot (Jun 28 2022 at 09:33):Basically you have to apply your Ltac1 thunk to s in the first definition.
Pierre Vial (Jun 28 2022 at 09:40):Huh, and how could I do this?
Pierre-Marie Pédrot (Jun 28 2022 at 09:40):You write an application?
Pierre-Marie Pédrot (Jun 28 2022 at 09:40):The syntax ltac1:(x |- foo) binds x into foo
Pierre-Marie Pédrot (Jun 28 2022 at 09:40):it's a closure, not a term that mentions some external x variable
Pierre Vial (Jun 28 2022 at 09:51):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?
Pierre-Marie Pédrot (Jun 28 2022 at 09:53):What's the intended content of s in your Ltac1 definition?
Pierre-Marie Pédrot (Jun 28 2022 at 09:53):A Coq term, an Ltac ident, something else?
Gaëtan Gilbert (Jun 28 2022 at 09:53):Ltac2 clearbody2 s := ltac1:(s |- clearbody s) (Ltac1.of_ident s).
Pierre Vial (Jun 28 2022 at 09:53):A Coq term of type string
Pierre-Marie Pédrot (Jun 28 2022 at 09:54):So indeed @Gaëtan Gilbert solution is the way to go.
Pierre-Marie Pédrot (Jun 28 2022 at 09:54):(you don't even have to define an intermediate Ltac2 def btw.)
Pierre Vial (Jun 28 2022 at 10:01):Mmh, unfortunately, I can't work with Coq's latest version on my project for now, so of_ident is yet unknown.
Pierre Vial (Jun 28 2022 at 10:02):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
Enrico Tassi (Jun 29 2022 at 14:47):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: Apr 20 2024 at 10:02 UTC