■

前置き

Software Foundationちょっとずつ読んでいるわけなんだけど、数日ハマっちゃった問題が解けた上で、なんかすごくチープな解法が見つかったような気がするのでそのことも含めて書く。あ、できればこっちで勉強会とか開けるようになったらいいなという気持ちもあって英語の方を読んでいるので、翻訳ではすでに処理されていたならごめんなさい。

Basicsの方ですでにやってあるのがbinaryという練習問題で、これは、binという新しい型を全ての要素が

• ゼロ
• すでにあるbinの要素の2倍
• すでにあるbinの要素の2倍足す1

になるように定義しなさいってことで、これは私でも簡単。

Inductive bin : Type := 
| bin_O : bin 
| bin_S0 : bin -> bin 
| bin_S1 : bin -> bin 
. 

あー、コンストラクタの名前とかもっとスタンダートなやつがありそうですが。bin_とか最初につけているのは自分が混乱しないため。

お次は、bin型のインクリメント

Fixpoint bin_inc (a : bin) : bin :=
match a with 
| bin_O => (bin_S1 bin_O)
| bin_S0 p => (bin_S1 p)
| bin_S1 p => (bin_S0 (bin_inc p))
end. 

次はbinからnatへの変換。

Fixpoint bin_to_nat (a : bin) : nat :=
match a with 
| bin_O => 0
| bin_S0 p => ((bin_to_nat p) + (bin_to_nat p))
| bin_S1 p => (S ((bin_to_nat p) + (bin_to_nat p)))
end. 

この時点で全てのb:binに対してbin_to_nat (bin_inc b)=S (bin_to_nat b)を証明しようとしてinductionないとできないよ～とかつぶやいていたんですが、どうも著者はこの時点では具体的なものに関してチェックさせるだけのつもりだったようです。

そんで本題のInductionの章のbinary_inverse。まず、natからbinへの変換。bin_incがすでにあるから余裕。

Fixpoint nat_to_bin (n : nat) : bin :=
match n with 
| O => bin_O
| S p => (bin_inc (nat_to_bin p))
end.

そんで、bin_to_nat (nat_to_bin n)=nを全てのn:natに対して示せ、っていうんだけど、これも問題なし。

次はnat_to_bin (bin_to_nat b)=bは必ずしも成り立たないと考察せよ、っていうもの。いや、だって普通にbin_to_nat bin_O=0だけど、2*0=0だからbin_to_nat (bin_S0 bin_O)=0ともなるわけで無理でしょ。だから、こういう無駄なbin_S0を除かないといけない。

というわけで、次の問題はnormalizeというbinからbinへの関数を定義して、nat_to_bin (bin_to_nat b)=normalize bとなるものを書きましょう、っていうんだけど。

本題

ようやく本題。このnormalizeって、normalize b=nat_to_bin (bin_to_nat b)で定義しちゃっていいの？って話。すなわち

Definition normalize' (a : bin) : bin := nat_to_bin (bin_to_nat a).

特にこれを禁止するような文が見当たらないんですけど、どうなんでしょ。

まじめに書いたのが

Fixpoint normalize (a : bin) : bin :=
match a with 
| bin_O => bin_O
| bin_S1 b => bin_S1 (normalize b)
| bin_S0 b => 
    match (normalize b) with 
    | bin_O => bin_O
    | bin_S0 c => (bin_S0 (bin_S0 c))
    | bin_S1 c => (bin_S0 (bin_S1 c))
    end 
end.

ちょっと前まで、bin_S1 b => bin_S1 bと書いていたので証明が通るわけもなかった。この関数を使った証明もようやく通った。汚いけどねぇ。absurdとかdiscriminateとかなしでも出来るんだろうけど…。

後書き

この辺りはサクサク終えられると思っていたのに、ここで詰まっちゃってにゃーにゃーしているところ。