読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

CoqでFizzBuzz

Inductive Definition refine apply

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では、その証明がある限り、どんなに複雑なプログラムに置いても、
実行結果にエラーが含まれることはない。