これ、やろうとすると結構難しい。
ということで勉強がてら、Web上の他の人のものを参考にして理解しながら進めることにしました。つまりほぼ私が書いたものではないです。いちおう自分でいろいろ調べつつ、理解できていないところは理解しながら進めてみました。
ちなみに参考にさせていただいたのは
CoqでFizzBuzz - にわとり小屋でのプログラミング日記 http://d.hatena.ne.jp/yoshihiro503/20070619
です。
多分、見た目ほぼ丸々一緒です。
私がいじくり回しただけです。
ただ、もとのと違うのは、受け取るものをnatにしてしまっています。一応最初私が作りたかったのはnatを受け取るものだったので。
Require Import Arith NPeano. Inductive FizzBuzzType : Set := |NumFb : nat -> FizzBuzzType |Fizz: FizzBuzzType |Buzz: FizzBuzzType |FizzBuzz: FizzBuzzType. (* forall a b : nat, {a mod b = 0} + {a mod b <> 0} *) Definition is_multiple_dec (a b: nat) := eq_nat_dec (a mod b) 0. (* nat -> Prop *) Definition is_fizz (num: nat) := (num mod 3) = 0. Definition is_buzz (num: nat) := (num mod 5) = 0. Inductive FizzBuzzProp : nat -> FizzBuzzType -> Prop := | R_numfb : forall n:nat, not (is_fizz n) -> not (is_buzz n) -> FizzBuzzProp n (NumFb n) | R_fizz : forall n:nat, is_fizz n -> not (is_buzz n) -> FizzBuzzProp n Fizz | R_buzz : forall n:nat, not (is_fizz n) -> is_buzz n -> FizzBuzzProp n Buzz | R_fizzbuzz : forall n:nat, is_fizz n -> is_buzz n -> FizzBuzzProp n FizzBuzz. (* forall n : nat, {r : FizzBuzzType | FizzBuzzProp n r} *) Definition fizzbuzz_n : forall n:nat, {r:FizzBuzzType | FizzBuzzProp n r}. refine (fun n => match (is_multiple_dec n 3, is_multiple_dec n 5) with | (right _, right _) => exist _ (NumFb n) _ | (left _, right _) => exist _ Fizz _ | (right _, left _) => exist _ Buzz _ | (left _, left _) => exist _ FizzBuzz _ end). apply (R_fizzbuzz n e e0). apply (R_fizz n e n0). apply (R_buzz n n0 e). apply (R_numfb n n0 n1). Qed.
今回のFizzBuzzをやってみて、Coqの型について勉強になりました。PropやSetといった基本的な型への知識不足やCoq.Init.Specif.sigといったまだ知らなかったものもたくさんありました。もっと型を意識して書かないとダメですね。
あと前日に書いたrefineタクティクもこのコードを見て初めて知りました。
実は、最初は単純な帰納的な定義をつかってパターンマッチをしてFizzBuzzを作ろうとしていたのですが、うまく証明できずに悩んでいました。Coq.Init.Specif.sigとrefineタクティクを使うとこんな感じで書けるのですね…
正直、関数型プログラミングへの慣れもまだまだ足りない感じです。Coqやりつつ、そちら側もしっかりつめていかなければ。。。