授業でBメソッドに入門してきた。 参考文献:「先端スキル開発特別講義?：形式手法を使ったデータ指向モデリングと検証」の資料 http://honiden-lab.ex.nii.ac.jp/u-tokyo/lecture2009/ BメソッドのツールであるAtelier Bのマニュアル http://www.atelierb.eu…

概要 Coqの些末な話。 proj2_sigの定義が読めなかったのでletについて調べた。 (* proj2_sig = fun (A : Type) (P : A -> Prop) (e : sig P) => let (a, b) as e0 return (P (proj1_sig e0)) := e in b : forall (A : Type) (P : A -> Prop) (e : sig P), P …

概要 鳩の巣原理(あるいはディリクレの箱入れ原理、部屋割り論法)の構成的な証明は、 1羽より多く鳩が入っている巣を見つけるアルゴリズムである。

概要 2回ハマったのでメモ。 eqの定義とパターンマッチ(の型アノテーション)の難しさのせいで、 eqがtransitiveであることの証明は意外に難しい。

概要 Coqの型クラスはレコード。普通の型と同様に使える。

(12/12更新) eq型のパターンマッチを使って型を書き換えるテクニックを 知ったので、mcomposeの書き直し。 型がMorphism A B -> Morphism B C -> Morphism A Cで、計算できるものができた。 ただし諸定理の定義をDefined.でTransparentにしておかないとうま…