2
$\begingroup$

To avoid tedious repetition I have a tactic that looks something like this:

Ltac unfolds := try unfold foo;
  try unfold bar;
  try unfold baz;
  apply some_lemma.

However, sometimes the expressions I would like to unfold are not in the goal, but in the hypotheses. I can make another tactic

Ltac unfolds' H := try unfold foo in H;
  try unfold bar in H;
  try unfold baz in H;
  apply some_lemma in H.

but is there a way to write my tactic so that it can (optionally) be used in hypotheses?

ie. so that I can write unfolds in H. in my proofs

$\endgroup$

1 Answer 1

4
$\begingroup$

I believe replacing your definition of unfolds' with

Tactic Notation "unfolds" "in" hyp(H) := ... should work. That's how stdpp defines a similar tactic (see line 305 in https://gitlab-10.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v.) You still have to define the tactic twice, once for the goal and once for hypotheses, but you should be able to use it in the way you want.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.