Coqで数学的帰納法

プログラムでリストや文字列を扱うことがあるが、これらに関する性質をチェックしたいと思ったらどうしたらよいだろうか？

例えばリストを逆順にするrevという関数を定義したときに、rev (rev l) = lという性質が、いかなるリストlでも必ず成り立つということを確認したいかもしれない。

リストや文字列は一般には有限ではないので、すべての場合をテストしてみることはとても現実的ではない。

こういうときには数学的帰納法を使って証明してしまうのが簡単だ。空列の場合とそうでない場合の2つの場合を証明すれば、任意のリストに関して証明できるので非常にお手軽で便利である。

試しにCoqで証明してみた。CoqはCIC(Calculus of Inductive Construction)という理論をベースにしているので数学的帰納法を簡単に扱うことができる。

まず rev 関数の定義。

  Fixpoint rev (l:list A) : list A :=
    match l with
      | nil => nil
      | x :: l' => rev l' ++ (x :: nil)
    end.

そして rev の rev が 元に戻ることの証明。

Theorem list_rev_rev : forall l : list A, rev (rev l) = l.
Proof.
intro l. (* l を仮定する *)
induction l. (* リストlの構造に関する帰納法 *)

(* (i).  l が 空リスト のとき *)
 simpl. (* βリダクション *)
   reflexivity. (* 構造が同じものは同じ *)

(* (ii). l が コンスの時 *)
simpl. (* βリダクション *)
  rewrite distr_rev. (* 補助的な定理distr_rev を使う *)
  simpl. (* βリダクション *)
  rewrite IHl. (* 帰納法の仮定を適用 *)
  reflexivity. (* 構造が同じものは同じ *)

Qed. (* 証明　終わり *)

ここで、distr_revはCoq のListライブラリにある基本的な定理で リストの結合とリバースに関する
基本的な性質である。

 distr_rev : forall x y:list A, rev (x ++ y) = rev y ++ rev x.

ソースコード全体は以下

Section ListRevRev.

Require Import List.
Open Scope list_scope.

Variable A : Set.

Theorem list_rev_rev : forall l : list A, rev (rev l) = l.
Proof.
intro l. (* l を仮定する *)
induction l. (* リストlの構造に関する帰納法 *)

(* (i).  l が 空リスト のとき *)
 simpl. (* βリダクション *)
   reflexivity. (* 構造が同じものは同じ *)

(* (ii). l が コンスの時 *)
simpl. (* βリダクション *)
  rewrite distr_rev. (* 補助的な定理distr_rev を使う *)
  simpl. (* βリダクション *)
  rewrite IHl. (* 帰納法の仮定を適用 *)
  reflexivity. (* 構造が同じものは同じ *)

Qed. (* 証明　終わり *)

End ListRevRev.