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 に答える