Bijection と invariant

　record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)　where
　 field
　　　 fun←　:　S → R
　　　 fun→　:　R → S
　　　 fiso← : (x : R)　→ fun← ( fun→ x )　≡ x
　　　 fiso→ : (x : S ) → fun→ ( fun← x )　≡ x

ですね。割と当たり前なんだが、

　　Bijection ℕ (ℕ ∧ ℕ) と Bijection ℕ ( List Bool )

後者は今年のお正月にやって、敗れさっていたらしい。ぜんぜん簡単なんですが、Agda で書くのはな。

なんですが、やっと invariant を書くのになれたみたい。

fun← ( fun→ x )　≡ x　を直接証明しようとすると、関数の引数を調整しながら

　 定義と同じように項 fun← ( fun→ x ) が展開されるようにする

というのが必要になるんですが、これがだいたいうまくいかない。なんだけど、

　record Invariant (i : S)　: Set
　 field
　　 j : R
　　 k1 : fun← i ≡ j
　　 k0 : fun→ j ≡ i

というように書いてやると、k1/k0 個別に調整できるので楽になるというわけ。induction で、Invariant を作れば完成と。

ま、証明の細かい面倒さは避けられないけど。

この Bijection は超準解析や集合の濃度でも使うからな。

これで、Agda の練習用の問題は一通りできた感じ。

　　素数が無限にある
　　素数の平方根が無理数

https://github.com/shinji-kono/automaton-in-agda