如何一步步检查 Coq 中更复杂的策略的作用？

我试图经历那些著名的和精彩的软件基础书籍 https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#lab30但我举了一个例子simpl. and reflexivity.只是在幕后做太多事情，阻碍了我的学习和理解。

我正在经历以下定理：

Theorem plus_1_neq_0 : forall n : nat,
  beq_nat (n + 1) 0 = false. (* n+1 != 0 *)
Proof.
  intros n.
  destruct n as [| n'].
    -simpl. reflexivity.
    -simpl. reflexivity.
Qed.

我真正想要的是能让我一步步经历的东西simpl. and reflexivity.做过。有什么东西可以让我这样做吗？

Destruct 应该解决以下问题：

因为 beq_nat 的第一个参数（这只是not equal i.e. !=) 进行匹配，但第一个输入取决于未知变量 n ，对于+所以匹配不能做任何事情，所以做simpl.让我们陷入困境（出于某种原因）。

显然它必须解决这个问题，因为 Coq 后来接受了证明。但如果仔细看第二个目标是什么，似乎又再次引入了与上面相同的问题：

2 subgoals
______________________________________(1/2)
beq_nat (0 + 1) 0 = false
______________________________________(2/2)
beq_nat (S n' + 1) 0 = false

现在我们有n'作为两者的第一个参数beq_nat and +再次。不过对于我这样的新手来说simpl.这次由于某种神秘的原因奇迹般地起作用了。我显然读过simpl. 文档 https://coq.inria.fr/refman/proof-engine/tactics.html?highlight=simpl#coq:tacn.simpl但作为一个新手，我真的不知道自己在寻找什么，而且对我来说形成对它的理解太密集了，这很有帮助......

无论如何，为什么它在这里起作用？我问的原因是因为我从来没有想过在这个示例证明上使用 destruct，特别是因为重复发生n'一个未知的变量，似乎能够看到真正发生的事情或不同的事情会很有用。所以我认为检查这些类型的事情的逐步分解会很有用（而不是每隔一天发布一个新的问题）。

注意我确实看到了这个问题：

coq 中的逐步简化？ https://stackoverflow.com/questions/39355817/step-by-step-simplification-in-coq

但我找不到一种方法让它对我有用，因为它是为该特定示例量身定制的。希望我的问题不会缩小到我的特定示例，尽管可能会这样，因为如果不知道如何进行逐步分解可能是不可能的simpl. (or reflexivity.）已经可以工作了（或者至少上述问题的上述答案给了我这样的印象）。

分解评估的一种方法是给出一个论据simpl，如建议的你链接的问题 https://stackoverflow.com/questions/39355817/step-by-step-simplification-in-coq. simpl f允许仅简化出现在调用下的子表达式f。在这种情况下，simpl Nat.add (or simpl plus or simpl "+"）简化S n' + 1 into S (n' + 1). Then simpl beq_nat turns beq_nat (S (n' + 1)) 0 into false.

As for reflexivity，它可以得出比较的两个项在简化后是否相等的结论，这意味着，如果我没记错的话，你总是可以替换simpl; reflexivity仅仅通过reflexivity.