I am new to Coq and to writing tactics, and I have been unable to figure out whether you can define more complicated tactics like the build in ones. For example, say that I have a tactic tac1 taking two arguments, and I define tac2 by
Ltac tac2 arg := tac1 arg _.
Then this works as I would expect, but I would really like to be able to call tac2 on a hypothesis, like tac2 arg in H. I can see that I can just give the hypothesis as an extra argument, but then I cannot use it in the goal, and I would also like to be able to use it like tac2 arg in *.
Is something like that possible, and how would it be accomplished?
I have found this answer about how you add intro patterns to tactics you define, and it lead me to this page about Tactic Notation, but I am unable to figure out from that if what I would like is possible.
Following this answer, you may define notations for tac2 like this:
Tactic Notation "tac2" constr(arg) :=
tac1 arg _.
Tactic Notation "tac2" constr(arg) "in" hyp(H) :=
tac1 arg _ in H.
Tactic Notation "tac2" constr(arg) "in" "*" :=
repeat match goal with
| H:_ |- _ => tac2 arg in H
| |- _ => tac2 arg
end.
Of course, tac1 needs to work with an in modifier and you should be careful with the termination of the repeat (see here).