GCD

冬休みのプログラミングです。Automaton の授業の例題に√2が無理数ってのをやろうとしていたらしいんだが...

　　gcd26 : (n m i : ℕ) → 1 < n → 1 < m　→ gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )

という簡単な部分で停まってます。割り算なんだけど、全部引き算で実装するわけなんだが、

　　gcd1 : ( i i0 j j0 : ℕ ) → ℕ
　　gcd1 zero i0 zero j0 with <-cmp i0 j0
　　... | tri< a ¬b ¬c = j0
　　... | tri≈ ¬a refl ¬c = i0
　　... | tri> ¬a ¬b c = i0
　　gcd1 zero i0 (suc zero) j0 = 1
　　gcd1 zero zero (suc (suc j)) j0 = j0
　　gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
　　gcd1 (suc zero) i0 zero j0 = 1
　　gcd1 (suc (suc i)) i0 zero zero = i0
　　gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))　j0 (suc j0)
　　gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0　

　　gcd : ( i j : ℕ ) → ℕ
　　gcd i j = gcd1 i i j j

と簡単なんだが、四つの引数の制約が足りないようだな。対称性とかは示せたんだが。

これができると、√2の他に素数が無限にあることとか、そんなのが証明できるはです。

そんなことをしながら大晦日か。