coq - 如何一步一步检查 Coq 中更复杂的策略？

Question

我试图通过著名的和精彩的software foundations book但我得到了一个例子，其中 simpl.和 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.和 reflexivity.做过。有什么可以让我这样做吗？

Destruct 假设可以解决以下问题:

because the first argument to beq_nat (which is just not equal i.e. !=) does a matching but the first input depends on a unknown variable n and the same thing for + so the matching can't do anything, so doing simpl. gets us stuck (for some reason).

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

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

现在我们有 n'作为 beq_nat 的第一个参数和 +再次。但是，对于我这样的新手， simpl.这次由于某种神秘的原因奇迹般地起作用了。我显然阅读了 simpl. documentation但作为这方面的新手，我真的不知道我在寻找什么，而且对我形成对它的理解很有帮助......

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

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

Step by step simplification in coq?

但我找不到一种方法让它对我有用，因为它是为那个特定的例子量身定制的。希望我的问题不会缩小到我的特定示例，尽管可能因为在不知道如何的情况下可能无法逐步分解 simpl. (或 reflexivity. )已经有效(或者至少上述问题的上述答案给了我这种印象)。

Answer 1

分解评估的一种方法是为 simpl 提供一个参数。 ，如 the question you linked 中所建议的. simpl f只允许简化出现在对 f 的调用下的子表达式.在这种情况下，simpl Nat.add (或 simpl plus 或 simpl "+")简化 S n' + 1进入 S (n' + 1) .然后simpl beq_nat转 beq_nat (S (n' + 1)) 0进入 false .

至于reflexivity ，可以断定被比较的两个项在化简之前是否相等，也就是说，如果我没记错的话，你总是可以替换simpl; reflexivity来自 reflexivity .