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

Question

我在想如何在COQ中使用simpl策略。
假设以下引理：

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

我不相信有可能效仿仅使用cbv的simpl战术，因为确实cbv delta不会让你选择哪个OCCURENCES更换，当它导致丝毫一步，而simpl只执行增量减少。 （参见https://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic135）

所以，即使非正式我们可以说，simpl进行通话这样的顺序，好像它可以访问执行这些削减比cbv战术暴露出什么下级的方式。