読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Coqでハノイの塔に関する証明

Coq ハノイ Tower of Hanoi

Coqが今流行っているらしい。

twitter経由で偶然ハノイの塔をCoq形式化している記事を見つけた。
なんか巷でCoqがはやっているようなので - 菊やんの雑記帳

なんかおもしろそうなので一つ簡単な命題を証明してみた。

証明したこと

Lemma answer_length : forall n from to rest,
   length (answer n from to rest) = pow 2 n - 1.

Coqのnat型は引き算がとっても難しいので, この手の証明はまず以下の補助的なLemmaを先に証明するのが吉だ。

Lemma answer_length_aux : forall n from to rest,
   length (answer n from to rest) + 1 = pow 2 n.

ただ、これはanswerの手数が2^n-1であることを示しただけで、それが最短手数である証明にはなっていないことに注意しよう。

証明の全体は以下のとおり。

(* 
http://github.com/kik/sandbox/blob/c1b16b684feb7482f0582480a43b2db4a9be3ce0/coq/Hanoi.v のコードと一緒に使ってね。
 *)

Fixpoint pow x n :=
  match n with
  | O => 1
  | S p => x * pow x p
  end.

Lemma answer_length_aux : forall n from to rest,
   length (answer n from to rest) + 1 = pow 2 n.
Proof.
induction n.
 reflexivity.
 
 unfold answer in |- *; fold answer in |- *.
 intros.
 rewrite app_length in |- *; rewrite app_length in |- *.
 rewrite <- plus_assoc in |- *.
 rewrite <- plus_assoc in |- *.
 rewrite IHn in |- *.
 rewrite plus_assoc in |- *.
 rewrite IHn in |- *.
 simpl in |- *.
 rewrite plus_0_r in |- *.
 reflexivity.
Qed.


Lemma answer_length : forall n from to rest, length (answer n from to rest) = pow 2 n - 1.
Proof.
intros.
rewrite <- (answer_length_aux n from to rest) in |- *.
rewrite plus_comm in |- *.
rewrite <- pred_of_minus in |- *.
simpl; reflexivity.
Qed.