您可以控制定义的展开使用透明和不透明命令。在您的示例中，您应该能够说出类似

You can control definition unfolding with the Transparent and Opaque commands. In your example, you should be able to say something like

Opaque Z.add.
simpl.
Transparent Z.add.

或者，参数 命令可用于指示 simpl 避免在某些情况下简化术语的策略。例如，

Alternatively, the Arguments command can be used to instruct the simpl tactic to avoid simplifying terms in certain contexts. E.g.

Arguments Z.add _ _ : simpl nomatch.

在您的情况下对我有用。这个特殊的变体所做的是避免简化一个术语，即在这样做之后，大的丑陋匹配会出现在头部位置（您在示例中所看到的）。但是，还有其他变体。

does the trick for me in your case. What this particular variant does is to avoid simplifying a term when a big, ugly match would appear in head position after doing so (what you saw in your example). There are other variants too, however.

最后，出于完整性考虑， Ssreflect 库为使某些定义在本地不透明提供了很好的基础架构。因此，您可以说类似

Finally, just for completeness, the Ssreflect library provides nice infrastructure for making certain definitions opaque locally. So you could say something like

rewrite (lock Z.add) /= -lock.

意思是锁定 Z.add ，所以它不会简化，然后简化表达式的其余部分（ / = 开关），然后再次解锁定义（ -lock ）。

meaning "lock Z.add, so that it won't simplify, then simplify the remaining of the expression (the /= switch), then unlock the definition again (-lock)".