久しぶりにAgda

なんか、沖縄とっても寒い〜

学生の方が一段落したので、いつものように Agda いじってるんですが。今回のお題は否定。有限の射を持つ圏、つまり、たんなるグラフがうまくできなくて、

＊　存在しない射に対する結合則とかは、矛盾⊥ から導くのが良いんじゃないか?

ってことで、否定について調べてたんですが、

　 Nope : (m n : ℕ) → Set
　 Nope (suc _) zero = ⊥
　 Nope _ _ = ⊤

　 nope : ∀ m n → m ≡ n → Nope m n
　 nope zero ._ refl = _
　 nope (suc m) ._ refl = _

　 peano : ∀ n → suc n ≡ zero → ⊥
　 peano _ p = nope _ _ p

　 http://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda

とかあって、結構面白い。

なんですが、

　 even : ℕ -> Set
　 even zero = ⊤
　 even (suc zero) = ⊥
　 even (suc (suc n)) = even n

　 div : (n : ℕ) -> even n -> ℕ
　 div zero p = zero
　 div (suc (suc n)) p = suc (div n p)
　 div (suc zero) ()

とかいうのもあって。()ってなんだ?

　 ¬_ : Set → Set
　 ¬ A = A → ⊥

　 data Dec (P : Set) : Set where
　 yes : P → Dec P
　 no : ¬ P → Dec P

　 EvenDecidable : Set
　 EvenDecidable = ∀ n → Dec (even n)

　 isEven : EvenDecidable
　 isEven zero = yes _
　 isEven (suc zero) = no (λ ())
　 isEven (suc (suc n)) = isEven n

　 http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type

とかやるらしく。起き得ない入力の組合せみたいなものらしい。Agdaが、これは起きないと理解してくれれば使えるらしいです。

つまり、A x B x C -> D みたいな関数で、A/B/Cのすべての入力について関数を定義する必要はないらしい。そういえば、data で規定された範囲しかみたいなみたいなことはやっていたな。どうせ、矛盾を取れる部分は規定された範囲外なんだから、実は除外できるんじゃないか?

今までは存在しない部分は Maybe で nothing とかやっていたんですが、それがいけなかったかも。で、演算定義とか結合則とから、いろいろ抜いていくと、

あれ? なんかできるじゃん

どうも、Maybe とかで record の中に入れ込んだので、Agdaが理解してくれなかったっぽい。

というわけで、要素2の圏を記述はきれいになりました。

なのだが、その後の Limit から Equalizer の証明には、はまりました。でも、定義を二重に入れてしまって、それの同一性が取れなかっただけで、定義を一部外に出したらできた。

　 http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/fd79b6d9f350/discrete.agda

結構、苦労していたのができて、ちょっとうれしいです。

　 http://seeker-s-eye.blogspot.jp/2017/01/agda.html