Coq：如何證明「a = b - > nat_compare a b = Eq。」？

Question

爲了掌握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. 

這給：（我也可以通過simpl，這似乎更有意義到達這個確切點）

1 subgoal 

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

現在

，與寫一篇文章，我只是聲稱這是我的證明通過電感..

我接近這在一個以正確的方式？我在哪裏可以最好地學習如何正確地做到這一點？

Answer 1

我能夠與

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

來證明這一點這裏的竅門是要離開歸納假設躺在身邊。 destruct是induction的較弱形式，它不會給出您需要用於此證明的歸納假設。