如何逐步检查在Coq中执行哪些更复杂的策略？ [英] How does one inspect what more complicated tactics do in Coq step-by-step?
问题描述
我正尝试浏览著名且精彩的软件基础书，但我举了一个例子，其中简化了。和自反性。只是做了很多事情，而且都是阻碍我的学习和学习理解。
I was trying to go through the famous and wonderful software foundations book but I got to an example where simpl. and reflexivity. just do to much under the covers and are hindering my learning & understanding.
我正在经历以下定理：
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.
我真正想要的是可以让我逐步了解简单。和自反性。做到了。
what I really want is something that allows me to go through step by step what simpl. and reflexivity. did. Is there something that allows me to do that?
Destruct应该解决以下问题：
Destruct is suppose to resolve the following issue:
是因为beq_nat的第一个参数（只是
不等于即！ =）进行匹配，但第一个输入取决于一个未知变量n，并且对于+也是相同的，因此匹配无法执行任何操作，因此，进行简化。会使我们陷入困境（出于某种原因）。
because the first argument to beq_nat (which is just
not equali.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 doingsimpl.gets us stuck (for some reason).
显然，由于Coq后来接受了证明，因此必须解决该问题。但是如果仔细观察第二个目标是什么，似乎会再次引入与上述相同的问题：
which it clearly it must resolve it since Coq later accepts the proof. But if one looks carefully what the second goal is, it seems that the same issue as above is re-introduced:
2 subgoals
______________________________________(1/2)
beq_nat (0 + 1) 0 = false
______________________________________(2/2)
beq_nat (S n' + 1) 0 = false
现在我们有 n'作为第一个参数再次是 beq_nat 和 + 。但是，对于像我这样的新手来说， simpl。这次奇迹般地由于某些神秘的原因而起作用。我显然读过 simpl。 文档，但是作为一个新手，我真的不知道自己在寻找什么，对我而言，形成浓厚的理解是有帮助的。
now we have n' as the first argument for both beq_nat and + again. However, to a novice like me, simpl. miraculously does work this time for some mysterious reason. I obviously read the simpl. documentation but being a novice in this I didn't really know what I was looking for and it was to dense for me to form an understanding of it that was helpful...
无论如何，为什么它在这里起作用？我要问的原因是因为对这个示例证明使用destruct永远不会发生，特别是 n'未知变量再次出现的原因，它似乎能够看到真正发生了什么或有什么不同将是有用的。因此，我认为逐步检查这些类型的事件很有用（而不是隔天发布新的SO问题）。
Anyway, why does it work here? The reason I am asking is because it would have never occurred to me to use destruct on this example proof, especially cuz of the re ocurrence of n' an unknown variable, and it seems that being able to see what really happened or what was different would be useful. So I thought checking a step-by-step break down of these type of things would be useful (rather than posting a new SO question every other day).
注意我确实看到了这个问题：
Note I did see this question:
Step by step simplification in coq?
，但我找不到一种方法可以使它对我是因为它是为特定示例量身定制的。希望我的问题不会局限于我的特定示例，尽管由于不知道 simpl。（或反身性。）已经起作用（或者至少上述问题的答案给了我这种印象）。
but I couldn't find a way to make it useful for me since it was tailored for that particular example to much. Hopefully my question doesn't become to narrow to my particular example, though it might since the step by step break down might not be possible without knowing how simpl. (or reflexivity.) works already (or at least the above answers to the question above gave me that impression).
推荐答案
一种分解评估的方法是给 simpl 一个参数，如您链接的问题。 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 。
One way to break the evaluation down is to give an argument to simpl, as suggested in the question you linked. simpl f allows to simplify only the sub-expressions that appear under calls to f. In this case, simpl Nat.add (or simpl plus or simpl "+") simplifies S n' + 1 into S (n' + 1). Then simpl beq_nat turns beq_nat (S (n' + 1)) 0 into false.
对于自反性，它可以得出比较中的两个术语是否相等的结论。直到简化为止，这意味着，如果我没记错的话，可以随时替换 simpl;。自反性只需自反性。
As for reflexivity, it can conclude if the two terms under comparison are equal up to simplification, which means that, if I am not mistaken, you can always replace simpl; reflexivity by just reflexivity.
这篇关于如何逐步检查在Coq中执行哪些更复杂的策略？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
