■

なんかいろんな言語で FizzBuzz が書かれているようなので、Coq でも書いてみる。

Coq の FizzBuzz は他のとは一味違う！なんとプログラムが正しく動くことが証明できるのだ！

とりあえず、書いたプログラム

Require Import Arith.
Require Import List.

(* FizzBuzz の結果を表すデータ型。FizzBuzz は list FizzBuzz_R を返す。 *)
Inductive FizzBuzz_R: Set :=
| R_nat (n: nat)
| R_Fizz
| R_Buzz
| R_FizzBuzz.

(* ループでまわす途中の値
 * r3: n を 3 で割った余り
 * r5: n を 5 で割った余り
 *)
Inductive FizzBuzz_D: Set :=
  FizzBuzz_d (n r3 r5: nat).

(* FizzBuzz_D を受け取って n+1 の FizzBuzz_D を返す。*)
Definition FizzBuzz_next (d: FizzBuzz_D) :=
  let (n, r3, r5) := d in
    let r3' := if eq_nat_dec r3 2 then 0 else r3+1 in
    let r5' := if eq_nat_dec r5 4 then 0 else r5+1 in
      FizzBuzz_d (n+1) r3' r5'.

(* FizzBuzz_D を受けとって FizzBuzz_R を返す。*)
Definition FizzBuzz_value (d: FizzBuzz_D) :=
  let (n, r3, r5) := d in
    (* n%3 と n%5 が 0 であるかで場合わけ *)
    match eq_nat_dec r3 0, eq_nat_dec r5 0 with
      | left  _, left  _ => R_FizzBuzz
      | left  _, right _ => R_Fizz
      | right _, left  _ => R_Buzz
      | right _, right _ => R_nat n
    end.

(* rep 回だけループする。*)
Fixpoint FizzBuzz_fold (rep: nat) (d: FizzBuzz_D) {struct rep} :=
  match rep with
    | O => nil  (* rep が 0 のときは空リスト *)
    | S k =>    (* rep が k の次の数の時は再帰する *)
      cons (FizzBuzz_value d) (FizzBuzz_fold k (FizzBuzz_next d))
  end.

(* 我々の FizzBuzz 関数 *)
Definition FizzBuzz (rep: nat) :=
  FizzBuzz_fold rep (FizzBuzz_d 1 1 1).

我々は割り算なんて複雑な関数は使わない。
だいたい、標準関数に n を m で割った余りが r かどうかを決定する関数が入ってないぞ！
（余りが r かどうかという命題はある。この二つは違うのだ！）

この FizzBuzz が正しい動作をすることを証明する前に、簡単な補題を証明する。

(* 簡単な補題
 * r=r' ならば r::L = r'::L
 *)
Lemma FizzBuzz_eq: forall (r r': FizzBuzz_R) L, r=r' -> r::L = r'::L.
Proof.
  intros.
  congruence.
Qed.

そして FizzBuzz の証明をするわけだが、残念なことにあまりに長いので途中を省略する。

(* 我々の FizzBuzz が正しい動作をすることの証明 *)
Theorem FizzBuzz_is_correct: FizzBuzz 100 =
R_nat 1::
R_nat 2::
R_Fizz::
R_nat 4::
R_Buzz::
R_Fizz::
R_nat 7::
R_nat 8::
R_Fizz::
R_Buzz::
R_nat 11::
R_Fizz::
R_nat 13::
R_nat 14::
R_FizzBuzz::
略
R_nat 98::
R_Fizz::
R_Buzz::nil.
Proof.
  compute.
  auto using FizzBuzz_eq.
Qed.

今回の証明法はいたって原始的だ。
証明したいことは
「FizzBuzz 100 = なんか結果のリスト」
なので、まず「compute」を使って、「FizzBuzz 100」を計算する。
そして、先に証明した補題を繰り返し使えば結果のリストが等しいことが証明できる。

ちなみに一般の n に対して、「FizzBuzz n」が正しいリストを返すかどうかはこの方法では証明できない（あたりまえだ。