Coqでハノイの塔に関する証明
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.