coq - 避免在假设和目标中应用策略的重复代码

Question

我发现我自己(有点)重复了代码，因为我希望在目标和假设匹配时采用相同的策略。例如:

match goal with
| H : PATTERN |- _ => simpl in H; rewrite X in H; ... ; other_tactic in H
| |- PATTERN       => simpl     ; rewrite       ; ... ; other_tactic
end.

如果比赛案例中的战术变长，我基本上会复制它，并带有一些 in添加了子句，这看起来很不令人满意，特别是如果我有很多匹配子句，以至于我重复了很多代码。
有时不是因为我匹配，而只是因为我定义了自定义策略，但根据上下文，我想将其应用于目标或命名假设。例如:

Ltac my_tac      H := simpl in H; rewrite X in H; ... ; other_tactic in H.
Ltac my_tac_goal   := simpl     ; rewrite X     ; ... ; other_tactic.

然后我再次“复制”代码。
有没有办法避免这种重复？
在某些时候我想知道目标有一个名字，比如 GOAL ，像假设，所以 simpl in GOAL相当于 simpl ，但我怀疑情况并非如此。在那种情况下，我可以放弃 my_tac_goal 的定义然后只需拨打 my_tac GOAL反而。
任何关于如何避免这种重复的建议将不胜感激。
PS 我很难想出一个好的标题，所以如果有人认为一个合适的，不要犹豫，改变它。

Answer 1

in 中目标的“名称”条款是 |- * ，但不知何故我在手册中找不到这方面的引用。例如。以下作品:

Goal 2+2=4 -> 2+2=4 -> 2+2=4.
intros H1 H2.
simpl in H1 |- *.

这简单地适用于 H1 和目标，但不适用于 H2。