如何从Coq假设'd = d + 1'证明`false`和扩展？

Question

Goal forall (d : nat), d + 1 = d -> False.
Proof.
  intros d H.
Abort.      

我怎样才能证明False从H？inversion H只是复制它.

Answer 1

以下是如何发现一些有用的引理来从你的上下文中得出一个矛盾.首先,我们需要导入一个包含它们的模块,否则Search命令将无法发现这些模块:

Require Import Coq.Arith.Arith.

让我们检查一下我们是否有我们需要的引理(回想一下,这x <> y是一个符号not (eq x y),并not A代表A -> False):

Search (?x + _ <> ?x).

这次没运气.好的,添加是可交换的,让我们这样尝试:

Search (_ + ?x <> ?x).

没有了.但我们当然应该有类似的东西:

Search (S ?x <> ?x).

最后我们有以下引理:

Nat.neq_succ_diag_l: forall n : nat, S n <> n

我们可以像这样使用:

Require Import Coq.Arith.Arith.

Goal forall (d : nat), d + 1 = d -> False.
Proof.
  intros d H.
  rewrite Nat.add_comm in H.
  now apply Nat.neq_succ_diag_l in H.
Qed.