Data.Fin と∀と∃

NFA 非決定性オートマトンの条件は、非決定的というだけあって集合から適当に取り出すということをします。

無限集合だと選択公理とかあるんだけど、有限集合なら全部調べればよい。というのをAgdaで書くのだが、これがはまる。

Fin n で n 個の自然数が取れるので、n から始めて 1 で終わるわけなんだけど、実際の要素は i-1 を使う。ややこしい。

条件に合うものを見つけて終わりなんだけど、なぜか、

　　0 に行った時にどうするか

が問題になる。それは起きないはずなんですが「それを証明する必要がある」。あぁ、まぁ、確かに。そうだよね。

あるとわかっていて探しているので「なかったら矛盾」で良いわけですけどね。なので、

　　「i>mの時はない」ってのをnから始めれば、m=0になった時に「あるって言ってたのにないじゃん」

と言えるというのに、昨日、Bar で飲みながら Agda を書いてた時に思いつきました。これで解決。

なのだが、これはテンプレだからライブラリにあるはずだよなと、Agda の Data.Fin を見ると、

　　¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
　　　　　　　¬ (∀ i → P i) → (∃ λ i → ¬ P i)
　　¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P)

とか三行で書いてある。いや、そこまで来るのに、いろいろあるので、これを使うかどうかは微妙なんだけど。

Agda まだ、知らないことたくさんあるらしい。

もう一つはまったのは、Data.Fin とData.Natの変換。

　　toℕ-fromℕ≤ : ∀ {m n} (m<n : m ℕ< n) → toℕ (fromℕ≤ m<n) ≡ m
　　toℕ-fromℕ≤ (s≤s z≤n)　　　 = refl
　　toℕ-fromℕ≤ (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ≤ (s≤s m<n))


これだな。自力で証明できるところまで来てライブラリにあることに気がつく、いつものパターン。