时间戳

首页 > 解决方案 > 避免重复代码以在假设和目标中应用策略

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

问题描述

我发现自己（有点）重复代码，因为我想在目标和假设匹配时采用相同的策略。例如：

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

如果 match case 中的策略变长了，我本质上就是复制它，加了一些in子句，这看起来很不满意，尤其是如果我有很多 match 子句，所以我复制了很多代码。

有时不是因为我匹配，而只是因为我定义了一个自定义策略，但根据上下文我想将它应用于目标或命名假设。例如：

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我很难想出一个好的标题，所以如果有人认为一个合适的，不要犹豫改变它。

标签： coq

解决方案

in子句中目标的“名称”是|- *，但不知何故我在手册中找不到对此的参考。例如以下作品：

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

这适用于 H1 和目标中的 simpl，但不适用于 H2。

推荐阅读