代数的構造と Coq:序

  • 4
    いいね
  • 0
    コメント
この記事は最終更新日から1年以上が経過しています。

Theorem Prover Advent Calendar 2014 20 日目の記事です。

代数的構造と Coq:序
http://mathink.net/program/coq_group.html

抽出されたソースコードはこちら

Setoid をベースにして二項演算子を備えたマグマを定義し、
そこから二通りの方法で群を構成していきます。

Structure とか Class の使用例でもあります。
使い分けの仕方には色々な作法があると思いますが、例えば私はこうしてるよ、というものです。
Coq で圏論をやったりこれを読んだりして、いい感じだなぁと思えたやり方です。

他にも色々な使い方があれば、色々試してみたいので教えていただけるとありがたいです。
Coq の機能の使い方は、証明したい対象によっても変わりますからね。

ちなみに "序" とついてはいますが、閉じた記事です。
個人的な予定としては "破" で準同型を扱い、 "急" で自分の書いてる圏論ライブラリに載せるつもりですが、いつになるかは全く以て不明です。

この投稿は Theorem Prover Advent Calendar 201420日目の記事です。