Stream: Coq users

Topic: clearbody of a list of lists of identifiers


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 &

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:07):

if you print the type of clearbody2 you'll see there is an issue

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:24):

Print Ltac2 foo. should do the trick, although it also prints the tactic.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:32):

The warning indicates that you haven't applied your function enough.

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:32):

As you can see from the type, the first argument is not used.

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:33):

Basically you have to apply your Ltac1 thunk to s in the first definition.

view this post on Zulip Pierre Vial (Jun 28 2022 at 09:40):

Huh, and how could I do this?

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:40):

You write an application?

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:40):

The syntax ltac1:(x |- foo) binds x into foo

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:40):

it's a closure, not a term that mentions some external x variable

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:53):

What's the intended content of s in your Ltac1 definition?

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:53):

A Coq term, an Ltac ident, something else?

view this post on Zulip Gaëtan Gilbert (Jun 28 2022 at 09:53):

Ltac2 clearbody2 s := ltac1:(s |- clearbody s) (Ltac1.of_ident s).

view this post on Zulip Pierre Vial (Jun 28 2022 at 09:53):

A Coq term of type string

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:54):

So indeed @Gaëtan Gilbert solution is the way to go.

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 09:54):

(you don't even have to define an intermediate Ltac2 def btw.)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jun 28 2022 at 10:03):

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

view this post on Zulip 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: Jan 27 2023 at 02:04 UTC