CoqでFizzBuzz
fizzbuzz.vの概要
Inductive FizzBuzzType : Set := | numb : A -> FizzBuzzType | Fizz : FizzBuzzType | Buzz : FizzBuzzType | FizzBuzz : FizzBuzzType. Definition is_fizz (a:A) := ismultiple_dec a A_three A_gt_three_zero. Definition is_buzz (a:A) := ismultiple_dec a A_five A_gt_five_zero. Inductive FIZZBUZZ : A -> FizzBuzzType -> Prop := | R_numb : forall n:A, not (IsMultiple n A_three) -> not (IsMultiple n A_five) -> FIZZBUZZ n (numb n) | R_fizz : forall n:A, IsMultiple n A_three -> not (IsMultiple n A_five) -> FIZZBUZZ n Fizz | R_buzz : forall n:A, not (IsMultiple n A_three ) -> IsMultiple n A_five -> FIZZBUZZ n Buzz | R_fizzbuzz : forall n:A, IsMultiple n A_three -> IsMultiple n A_five -> FIZZBUZZ n FizzBuzz. Definition fizzbuzz_n : forall n:A, {r:FizzBuzzType | FIZZBUZZ n r}. refine (fun n => match (is_fizz n, is_buzz n) with | (right h11, right h12) => exist _ (numb n) _ | (left h21, right h22) => exist _ Fizz _ | (right h31, left h32) => exist _ Buzz _ | (left h41, left h42) => exist _ FizzBuzz _ end). (*1*) apply (R_fizzbuzz n h41 h42). (*2*) apply (R_fizz n h41 h22). (*3*) apply (R_buzz n h31 h32). (*4*) apply (R_numb n h31 h12). Qed.
コンパイルと実行の様子
yoshihiro$ coqc fizzbuzz.v yoshihiro$ ocamlc coqfizzbuzz.ml main.ml yoshihiro$ ./a.out 1 2 Fizz 4 Buzz Fizz 7 8 Fizz Buzz 11 Fizz 13 14 FizzBuzz 16 17 Fizz 19 Buzz Fizz 22 23 Fizz Buzz 26 Fizz 28 29 FizzBuzz 31 32 Fizz 34 Buzz Fizz 37 38 Fizz Buzz 41 Fizz 43 44 FizzBuzz 46 47 Fizz 49 Buzz Fizz 52 53 Fizz Buzz 56 Fizz 58 59 FizzBuzz 61 62 Fizz 64 Buzz Fizz 67 68 Fizz Buzz 71 Fizz 73 74 FizzBuzz 76 77 Fizz 79 Buzz Fizz 82 83 Fizz Buzz 86 Fizz 88 89 FizzBuzz 91 92 Fizz 94 Buzz Fizz 97 98 Fizz Buzz yoshihiro$
Coqでは、その証明がある限り、どんなに複雑なプログラムに置いても、
実行結果にエラーが含まれることはない。
