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

Question

我的问题是:为什么“直觉”在我的例子中起作用？

我正在努力证明

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获得证明脚本，但我听说它不再起作用了。也许你可以尝试一下。您随时可以Show Proof之后intuition获得证明术语，但它不会告诉您所使用的策略。

在您的特定情况下，通过引入 S n = S m 证明非常简单从目标结束开始，使用 injection就可以得到n = m在上下文中，然后导出与 (n =? m) = false 的矛盾.

xywang 的编辑:任何形状的陈述 A <> B只是 A = B -> False 的语法糖。因此，intros战术可以应用于任何目标P1 -> ... Pn -> A <> B ，与 n+1 (注意 +1 )名称。例如考虑:

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

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

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