二進数のnormalizeに関して、normalizeした二進数が必ずnormalizeする前のものより短くなることを証明してみた。 証明することは出来たが、命題に対する帰納法ってやつをあんまり理解していないことが分かった。(最初、n S n 帰納法でやってしまって泥沼に嵌…

coqのワイルドカードって、データしかあかんのか？ Fixpoint bin_len (b : bin) : nat := match b with | Q => O | T b' => S (bin_len b') | F b' => S (bin_len b') end.を Fixpoint bin_len (b : bin) : nat := match b with | Q => O | _ b' => S (bin_l…