昨日 (http://lkozima.hatenablog.com/entry/2013/07/19/225156) よくわからないとか言っていたのが冷静に考えたらできた。なんかこういうのを考えていて， Inductive mov : nat -> nat -> Prop := | mov_1 : forall m, mov (S m) m | mov_2 : forall m, mov…

……が，期待通りに生成されないと思ったけどよく考えてみるとどうなるべきなのかわからなかった話。 準備 例として，石取りゲームみたいなのを考えます。いくつかの石があって，一度に三つまで取ってよいということにしましょう。そうすると，プレイヤーのと…

型健全性というと type preservation と progress が成り立ってればよいというのがよくある話ですが，それでなぜ健全といえるのかというところをわざわざ形式的に書いてみた話です。といっても，わかりやすい説明をしようという気はあまりなくて，知ってる人…

道を歩いているとき，無意識のうちに数字をいじっていることに気付いたのでその内容を思い出しながら書いてみる試み。42 と 105 は確かどっちも異なる三つの素数の積である。2, 3, 5, 7 から三つ選んでかけるとそれらが出てくる。だけどどっちもそこそこ小さ…

久しぶりに Coq を触っててしばらくはまった話。とりあえず準備。 Require Import Program. Set Implicit Arguments. Inductive fin : nat -> Set := | First : forall n, fin (S n) | Next : forall n, fin n -> fin (S n).fin n はサイズ n の有限集合の型…

「構成的プログラミングの基礎」という本を読んでいたら choice principle のことが書いてあって，この間書いた直観主義と選択公理のことと一見噛み合わない内容だったので，どういうことか考えてみた話を。 Choice Principle 次の公理のことを choice princ…

下記の講義ノートを読んでいたら選択公理のことが書いてあって，それがおもしろかったのでこの記事を書こうとしています。http://math.andrej.com/2005/08/23/realizability-as-the-connection-between-computable-and-constructive-mathematics/直観主義と…

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

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 が何を…