Search code examples
coqcoq-tactic

Using `<tactic> in <Hypothesis>` pattern for user defined tactics


There are many tactics in the standard library, such as the simpl_list, simpl_map, etc. which do not have a in form. This is awkward, because many a times, I'd like to run simpl_list within the context of a hypothesis.

Is there some way to enable this?


Solution

  • For your specific example, simpl_list is just autorewrite with list so you can do autorewrite with list in H. I don't see simpl_map in the standard library.

    Unfortunately there's no general way to take a tactic and run it in another context (specifically, the in H, in *, and in *|- variants the builtin tactics tend to provide). It's also a fairly manual process to write each of these variants and use Tactic Notation to give the same syntax, which is why you don't always see all the variants.