简单策略在 COQ 中有什么作用

Question

我想知道该simpl策略如何在 COQ 中发挥作用。
假设以下引理：

Parameter n:nat. 
Lemma test: S n + 0 = S (n+0).

现在，simpl.战术产生

S (n + 0) = S (n + 0)

我的理解是simpl执行一系列 cbv beta, delta, iota转换。我试过了，但无法获得与simpl. 基本问题是，在cbv delta展开之后，该plus术语一直在展开。我怎样才能去扩展它，即重新替换plus扩展定义的名称？
或者，谁能告诉我如何simpl通过手动执行更基本的策略来获得效果？

Answer 1

我不认为可以simpl使用 only 来模拟该策略cbv，因为确实cbv delta不允许您选择要替换的事件，而simpl仅在导致 iota 步骤时执行增量减少。（参见https://coq.inria.fr/distrib/current/refman/proof-engine/tropics.html#coq:tacn.simpl）

因此，即使我们非正式地可以说它simpl执行了这样的一系列调用，但它似乎可以使用比该cbv策略所公开的更低级别的方式来执行这些减少。