Stream: Coq users

Topic: current goal name


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

view this post on Zulip Joachim Breitner (Dec 04 2020 at 12:15):

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Dec 04 2020 at 12:58):

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

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

view this post on Zulip Joachim Breitner (Dec 04 2020 at 13:31):

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

view this post on Zulip Joachim Breitner (Dec 04 2020 at 13:34):

(deleted)

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