coq - 简单策略在 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仅使用策略 cbv ，因为确实cbv delta不允许您选择要替换的事件，而 simpl仅在导致 iota 步骤时才执行 delta-reduction。 (参见 https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.simpl)

所以，即使非正式地我们可以说 simpl执行这样一系列的调用，似乎它可以访问执行这些减少的较低级别的方式，而不是 cbv战术暴露。