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

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。