存在の証明 1

Coqをインストールしたので
http://d.hatena.ne.jp/qnighy/20101220/1292829222
この辺を参考に勉強中です。
ついでに自分で命題を考えて証明してみた。

命題は forall (x : nat), x > 1 -> x < x * x. というもの。

こんなもの直感的だろ！
といいたい所ですが、論理学の世界では公理系から演繹（証明）出来ないものは全て不定な存在です。

戦略的にはSearchPatternで　(_ < _ * _) を調べ見つけた

mult_lt_compat_r: forall n m p : nat, n < m -> 0 < p -> n * p < m * p

の定理を使う方針で証明していきます。
pをx、nを1、mをxとすると仮定から p n mはnatであり、n < mとなるので定理より命題は成り立ちます。
が、 x < x * x と 1 * x < x * xが同値な命題かどうかを証明しなければなりません。
要は x = 1 * xを証明する必要があります。
証明の途中で仮定化したい補題が発生した場合はassert tacticsでがしがし仮定化し証明していきます。

では証明

Lemma square_is_big:
 forall (x:nat), x > 1 -> x < x*x.
Proof.
 intros.

 (* x = x * 1 の証明 *)
 assert (G: x = x * 1).
 assert (G1: x * O = O).
 apply (mult_0_r x).
 assert (G2: x = x + O).
 apply plus_n_O.
 rewrite G2 at 1.
 assert (G3: x + O = O + x).
 apply plus_comm.
 rewrite G3.
 rewrite <-G1 at 1.
 apply (mult_n_Sm x O).

 (* x < x * x を 1 * x < x * x に変換 *)
 rewrite G at 1.
 assert (G4: x * 1 = 1 * x).
 apply mult_comm.
 rewrite G4.

 (* x > 1 は仮定に存在しているので,後は仮定にx > 0が必要なので証明 *)
 assert (G5: x > 0).
 assert (G6: 1 > 0).
 apply neq_O_lt.
 apply O_S.
 apply (gt_trans x 1 O).
 exact H.
 exact G6.

 (* 条件が整ったので最後の仕上げ *)
 apply mult_lt_compat_r.
 exact H.
 exact G5.
Qed.

x = x * 1とか 1 > 0とかの証明が意外に難しかった。
まぁただ欲しい仮定はassertでどんどん証明していくという事を掴めればなんとかなる。
普通に数学の命題を証明する時と同じ思考回路を使うんだけど SearchPatternで公理、定理を検索出来るからかなり便利。