我的问题是:为什么'直觉'在我的例子中起作用？
我想证明
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
那么'直觉'/'firstorder'/'auto'都可以解决当前的目标.
但为什么他们工作？Coq手册说他们会进行一些搜索工作.这是否意味着它可以用其他一些简单的策略重写？
谢谢!
编辑:可以看出我在上面的证明中对n和m应用了归纳法.根据@Vinz的回答,它没有必要进行这样的归纳过程.intros在第一步和intro目标n <> m,它将产生一个矛盾的假设H.
战术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