ユークリッドの互除法

√2 が無理数な証明には n^2 | 2 なら n | 2 ってのを使うわけですが、2 で証明するのは、まぁ、難しくない。

2でなくて一般的な素数でやろうと思うと良くわからない。ぐぐったら素因数の一意性を使うとか出てくるんですが、

その一意性の証明ってやさしくないよね? と思ったら、

　　ユークリッドの定理 素数 p なら (n * m) | p → (n | p) ∨ (n | q)
　　ユークリッドの補題 a x + b y = gcd x y

ってのを使うらしい。これを証明するのに素因数の一意性を使ってはいけませんなわけね。

で、これを証明するには互除法を追っていくことになるらしい。

すると、やはり、Hoare Logic 的に不変条件を持ち歩くということになる。

結局、プログラムの正しさの証明に戻ってくるわけね。

Agda で書いてみたんですが、整数使わないとだめだな。整数の利点は a - b で a > b を確認しなくて良いところだな。

まぁ、既にライブラリにはあるので、練習あるいは証明法の確認みたいな感じです。