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.