我想知道简化策略在COQ中如何运作.

假设以下引理：

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

现在,简单.策略产生

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

我的理解是,simpl执行一系列的
cbv beta,delta,iota转换.
我尝试过,但无法获得与简单相同的结果.基本问题是在cbv delta扩展后,加号项不断扩大.如何对其进行去扩展,即重新替换扩展定义的加号？
或者,任何人都可以告诉我如何通过手动执行更基本的策略来获得简化的效果？

最佳答案 我不相信只使用cbv来模拟简化策略是可能的,因为确实cbv delta不允许你选择要替换哪些出现,而简单只在它导致iota步骤时执行delta减少. (参见
https://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic135)

因此,即使非正式地我们可以说simple执行这样的一系列调用,它似乎可以访问比cbv策略暴露的更低级别的执行减少的方式.