1

为了了解 Coq 是什么，我最终遇到了一种情况，我基本上需要证明a=b -> nat_compare a b = Eq.

我可以通过以下方式轻松开始：

Coq < Theorem foo: forall (a:nat) (b:nat), a=b->nat_compare a b=Eq.
1 subgoal

============================
forall a b : nat, a = b -> nat_compare a b = Eq

foo < intros. rewrite H. destruct b.

这给了我：

2 subgoals
a : nat
H : a = 0
============================
nat_compare 0 0 = Eq

subgoal 2 is:
nat_compare (S b) (S b) = Eq

第一个是微不足道的：

foo < simpl. reflexivity.

但下一个目标难倒我：

1 subgoal

a : nat
b : nat
H : a = S b
============================
nat_compare (S b) (S b) = Eq

我可以

foo < rewrite <- H.

这使： 

1 subgoal

a : nat
b : nat
H : a = S b
============================
nat_compare a a = Eq

（我也可以通过 到达这个确切的点simpl，这似乎更有意义。）

现在，用笔和纸，我只是声称这是我的归纳证明..

我是否以正确的方式处理这个问题？我在哪里可以最好地学习如何正确地做到这一点？

4

1 回答 1

2

我能够证明这一点

Theorem triv : forall a b, a = b -> nat_compare a b = Eq.
  intros; subst; induction b; auto.
Qed.

这里的诀窍是将归纳假设留在周围。destruct是一种较弱的形式，induction它不会为您提供此证明所需的归纳假设。

于 2013-10-30T13:17:28.927 回答