如何逐步检查Coq中更复杂的策略？

Question

我试图去通过著名的和精彩的软件基础的书,但我到这里的例子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可以解决以下问题:

因为第一个参数beq_nat(这只是not equal如!=)不匹配,但第一输入取决于未知的变量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和+试.然而,对于像我这样的新手来说,simpl.出于某种神秘的原因,这次奇迹般地起作用.我显然阅读了simpl. 文档,但作为一个新手,我真的不知道我在寻找什么,而且我要密切地形成一个有用的理解...

无论如何,为什么它在这里工作？我问的原因是因为我在这个示例证明中使用destruct从未发生过,特别是n'对于未知变量的重现,并且看起来能够看到真正发生的事情或者不同的事情将是有用.所以我认为逐步分解这些类型的东西会很有用(而不是每隔一天发布一个新的SO问题).

---

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

在coq中逐步简化？

但我无法找到一种方法让它对我有用,因为它是为那个特定的例子量身定制的.希望我的问题不会成为缩小到我的特殊例子,虽然它可能因为一步一步打破不知道也许是不可能的如何simpl.(或reflexivity.)工程已经(或至少上述问题的答案上面给我的印象).

Answer 1

逐步减少这个：

beq_nat (S n' + 1) 0 = false

  (* Without the `+` notation, which is purely for pretty-printing: *)

beq_nat (plus (S n') 1) 0 = false

  (* by definition of plus:   plus (S n') 1 = S (plus n' 1) *)

beq_nat (S (plus n' 1)) 0 = false

  (* by definition of `beq_nat`,

     beq_nat (S (plus n' 1)) 0 =
     = match S (plus n' 1) with
       | O => ... (* unreachable *)
       | S m => match 0 with
                | O => false
                | S _ => ...
                end
       end
     = match 0 with
       | O => false
       | S _ => ...
       end
     = false
  *)

false = false