为什么 'intuition' 在 Coq 的例子中有效？

Question

我的问题是：为什么 'intuition' 在我的示例中有效？

我要证明

Lemma eqb_false : forall n m : nat, eqb n m = false -> n <> m.

在最后一步，我可以看到

n : nat
IHn : forall m : nat, (n =? m) = false -> n <> m
m : nat
IHm : (S n =? m) = false -> S n <> m
============================
 (n =? m) = false -> S n <> S m

然后'intuition'/'firstorder'/'auto'都朝着当前目标努力。

但它们为什么起作用？ Coq 手册说他们将进行一些搜索工作。是不是说可以用其他一些简单的战术改写？

谢谢！

编辑： 可以看出，我在上面的证明中对 n 和 m 应用了归纳法。根据@Vinz 的回答，没有必要进行这样的归纳过程。 intros在第一步和intro在n <> m的目标，它会产生一个矛盾的假设H.

Answer 1

像 intuition、firstorder 或 auto 这样的策略试图通过一些自动推理来解决你的目标，但你总是可以用你手工制作的证明替换他们的证明之一。

在以前的 Coq 版本中，您可以执行 info intuition 来获取证明脚本，但我听说它不再起作用了。也许你可以试试。你总是可以在 intuition 之后 Show Proof 得到证明项，但是它不会给你使用的策略。

在您的特定情况下，通过从目标末尾引入 S n = S m 并在其上使用 injection 在上下文中获得 n = m ，证明非常简单，并且然后推导出与 (n =? m) = false.

的矛盾

编辑 xywang：任何形如 A <> B 的语句都只是 A = B -> False 的语法糖。因此，intros 策略可以应用于任何具有 n+1（注意 +1）名称的目标 P1 -> ... Pn -> A <> B。例如考虑：

=============================
 P -> Q -> A <> B

通过应用策略 intros p q eqAB.，目标变为

p : P
q : Q
eqAB : A = B
=============================
False

为什么 'intuition' 在 Coq 的例子中有效？

Why 'intuition' works in the example of Coq?

coq