[Coq] ASN.1 Library is under construction

　この連休にCoqの練習がてら作っていたASN.1のライブラリで、全然完成してないのだがとりあえず出来たところまで公開。
　Coqdocで生成したドキュメントがTLV.htmlです。（コードが成長したら随時更新予定）

　ASN.1が何かについては、A Layman's Guide to a Subset of ASN.1, BER, and DERあたりを読んで下さい。電子証明書とかで使っているバイナリフォーマットなので、証明付きのライブラリを作りたいのだ。

　本当は

Inductive tlv_value : Set := 
| Primitive : string -> tlv_value 
| Structured : list tlv -> tlv_value
.

みたいに定義したかったのだが、そうするとtlv_value, tlv に関する帰納法をうまく構成出来なかった。まだCPDT Chapter 3の読み込みが足りないのだろうなぁ。
　が、とりあえず幾つかの定理も証明できたし、出だしとしてはこんなものかもとも思う。

　Coqを勉強しようと思う様なプログラマの人は、ある程度複雑な型（相互再帰的だったり再帰がネストしていたり）を定義出来ると思うが、Coqは帰納型に対して帰納法を与える関数が作れないと駄目で、しかしそこが実は難しい、というのがこの連休に得た知見だ。