Hi! Is there a way in LTac to get the name of the current goal? I.e. the thing that
refine ?[foo] would set?
And, somewhat relatedly, can I do string operations on identifiers in Ltac?
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?
You can geenrate a fresh evar with a name and then unify it with the goal afaik
It's one of the typical uses of Ltac2 actually.
See e.g. https://gitlab.mpi-sws.org/iris/string-ident/-/blob/master/theories/ltac2_string_ident.v for this kind of hacks
string_to_ident works nicely… now I wonder how I can have
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: Oct 01 2023 at 17:01 UTC