線型論理のおはなし。線型論理は少しかじった程度でまったく詳しいわけじゃないのでこれから書く内容が的外れである可能性もあると思いますが，以前からなんとなく思っていることを書いてみます。線型論理には「かつ」と「または」がそれぞれ二種類あり，加…

http://www.youtube.com/course?list=EC6763F57A61FE6FE8なんとなく英語を聞きたくなって適当に検索したら出てきたので見たのですが，いい講義なんじゃないかと思いました。大学の数学の講義って，どこもそうなのかは知らないのですが少なくともぼくが受けた…

証明がうまくいかなくて工夫が必要な事例を集めようとしています。今回のは Coq'Art にも似たような例が書いてあった気がしますが。 問題設定 Z -> Z な関数 f と，Z -> Prop な述語(「よい」整数の定義)が与えられます。 0 書けたら，sum の値は証明の中身…

Coq のモジュールシステムについて，使い方がいまいちつかめてない気がしたので stdlib でどう使われてるのか見てみました。はじめに，モジュールとはどういうものかを一応言語化してみる。Coq の module はまあいわゆる module だと思っていればよいと思う…

依存型を使っていると destruct が ill-typed term を作って失敗することがあるんですが，その原因が何なのかがよくわからないので似たような現象を起こす小さな例を探しています。pattern でおそらく同様の原因によるものと思われるエラーが出る例を作りま…

前回のうまくいかない elim の続きで，Coq'Art 15 章に載っている方針による別証明について。なぜそっちはうまくいくのか。ちなみにここに書くことが Coq'Art にきちんと解説されていたかどうかは覚えていませんが，こういうことを細かく解説したものを読ん…

tactic が proof term を生成していく様子を何度か観察しましたが，何のためにそんなことをしていたかというと，ときどき tactic が失敗してよくわからないエラーを出すことがあるのでその理由を知りたかったのです。今回はそこに近づこうとしてみます。例と…

Coq.Sets.Ensembles がなんだかうまく使えないなあ，と思った話。ちなみに以下で使う諸定義は http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html を必要に応じて参照してください。具体的には何かというと， Coq < Goal forall x : A, forall X : Ensembl…

append の結合性の別証明。f_equal を使ったらどうなるかやってみました。 Coq < Goal forall A (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs. 1 subgoal ============================ forall (A : Type) (xs ys zs : list A), xs ++ ys ++ zs …

今度は等式の証明でやってみました。append の結合性。 Coq < Goal forall A (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs. 1 subgoal ============================ forall (A : Type) (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs…

今度は算術でやってみました。 Coq < Goal forall n, n = 0 \/ 1 <= n. 1 subgoal ============================ forall n : nat, n = 0 \/ 1 <= n こんなのを証明してみましょう。帰納法に決まってるので帰納法を使います。 Unnamed_thm < induction n. 2 s…

一月の終わりごろから Coq で遊んでいます。あまり自明でないこともだんだんできるようになってきた気がしますが，なにかがわかるようになってくるということとなにかがわからないと気付くこととはたいていの場合同時に起こることのようです。tactic が何を…