Agdaの証明法

素数が無限にあること証明はゲンツェンの最初の記号論理的な証明の例なので由緒あるものなんですが、ちょっとやってみてるけど

割とめんどい。ちなみにWikipedeiaはまともなんだが、それがいがいのは割といい加減なのが多いみたいです。

　　n と n + 1 は互いに素

みたいなのを使う方法もあるらしい。でも階乗使う普通の方法で。

その中で、n! は n 以下のすべての数で割きれるっていう簡単なのがあるのだが....

　　すべての数で割きれるってので再帰する必要がある

「n<mのすべてのnで割きれる」という関数を再帰で作る的な方法を最初に思いつくわけですが、

　　何で割り切れるかを返す関数
　　それで割きれる証明を返す関数

と二つ作る必要がある。良くあるパターンなのだが、

　　二つの関数を同時に展開して、展開した形になって欲しい

わけですが、ならないことが良くある。場合分けが重複してたりするとか、with での仕分けとか。これはλ計算の理論の範囲外ではあるけどね。

まぁ、何か研究があるとは思うんだが、Agda にはそれを制御する方法ないらしい。

割きれるという record を作って、それを再帰的に作っていくという方法がある。それだと割と簡単。 一種の分割統治かとも思うけど。

平行展開みたいな方法はだめな方法らしい。自然ではあるんだけど。

あと、もう少しだが GCD 側でやり残したものがあるっぽいな。