Thursday 2 March 2017

久しぶりに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

No comments: