Stream: Coq users

Topic: current goal name

Joachim Breitner (Dec 04 2020 at 12:13):

Hi! Is there a way in LTac to get the name of the current goal? I.e. the thing that refine ?[foo] would set?

Joachim Breitner (Dec 04 2020 at 12:15):

And, somewhat relatedly, can I do string operations on identifiers in Ltac?

Joachim Breitner (Dec 04 2020 at 12:28):

More concretely, what I have is this

Ltac name_cases :=
  lazymatch goal with
  | [ H : CaseName |- _ ] => refine [?H]; clear H
  end.

which kinda works.

But I want to mangle the name of the hypothesis before, and write something like this (and variations therefore):

Ltac name_cases prefix :=
  lazymatch goal with
  | [ H : CaseName |- _ ] => refine [?(prefix ++ " _ " ++ H]; clear H
  end.

But that doesn't quite work…
(And maybe such kind of munging of identifiers is simply not supported)

Maybe Ltac2 is better for that?

Fabian Kunze (Dec 04 2020 at 12:47):

You can geenrate a fresh evar with a name and then unify it with the goal afaik

Pierre-Marie Pédrot (Dec 04 2020 at 12:58):

It's one of the typical uses of Ltac2 actually.

Pierre-Marie Pédrot (Dec 04 2020 at 13:00):

See e.g. https://gitlab.mpi-sws.org/iris/string-ident/-/blob/master/theories/ltac2_string_ident.v for this kind of hacks

Joachim Breitner (Dec 04 2020 at 13:31):

Neat! string_to_ident works nicely… now I wonder how I can have ident_to_string :-)

Joachim Breitner (Dec 04 2020 at 13:34):

(deleted)

Yannick Forster (Dec 04 2020 at 13:36):

Probably every meta-programming approach for Coq has such a function, where PMP's repo you linked is an OCaml solution to the problem. Here's the MetaCoq solution for it: https://github.com/uds-psl/metacoq-examples-coqws/blob/968d19601bcd662e51c75cc606fb6c50e9014508/metacoq-nested-induction/MetaCoqInductionPrinciples.v#L20

Last updated: Apr 19 2024 at 18:01 UTC