ひとり勉強会

ひとり楽しく勉強会

2010-01-01から1年間の記事一覧

Coqの入門記事を書く会 (4)

Coq

今回は、入門記事書きはちょっと休憩して、Coqの解説記事などを集める会です。 英語 言語そのものを浅く/深く眺めていく、という方向のテキスト3つ: Coq in a Hurry 「忙しい人のためのCoq入門」。比較的よくまとまっている気がしました。 Coq Proof Assis…

自然数とリスト: まとめ (3.7)

Coq

駆け足でいろいろ紹介しました。 SearchAbout でライブラリを検索 自然数やリストはInductiveなデータ = に関する証明 reflexivity, symmetry, transitivity, discriminate = を使った書き換え rewrite, replace 計算をすすめる simpl, cbv, ... 自動証明 om…

自然数とリスト: exists (3.6)

Coq

ここまで forall, ->, and, or, not のCoqでの使い方を見ました。Wikipediaの一階述語論理のページなどを見てみると、もう一種類、この手の論理結合子があります。∃(存在する)。Coq では、exists と書きます。 Theorem even_or_odd: forall (n:nat), exist…

自然数とリスト: 帰納法の色々 (3.5)

Coq

Coqでの帰納法の仕組みについて、ちょっとだけ。CoqIDE に Inductive nat := | O : nat | S : nat -> nat.と打ち込んで nat を再定義してみてください。 nat is defined nat_rect is defined nat_ind is defined nat_rec is definedこう右下に表示されると思…

自然数とリスト: 帰納法 (3.4)

Coq

別の問題を証明してみましょう。Anarchy Proof から Sum of natural numbers をお借りします。ring を使わないでやってみよう、という問題ですが、気にせずringを使って解いちゃいますので、ネタバレにはなっていないはず…。 Require Import Arith Omega. Fi…

自然数とリスト: 自動証明 (3.3)

Coq

Coqさんは非常に賢いので、実は、今回くらいの証明は自動でやってくれます。 Proof. intros. omega. Qed.omega はプレスバーガー算術という美味しそうな名前の理論の簡易全自動ソルバーで、整数に関する等式や不等式のかなりの部分を自動的に証明してくれま…

自然数とリスト: rewriteなど (3.2)

Coq

x=0の場合は終わったので、残ったゴールはこれです。 ------------------------- S x < S x + S xこれを証明するには…なにか、このくらいはさっきImportしたArith標準ライブラリで証明されていないでしょうか。CoqIDEでは SearchAbout (_ < _ + _).と打ち込…

自然数とリスト: Inductive (3.1)

Coq

前回、andやorなどの命題が"Inductive"で作られてることをご紹介しました。Coqでは、命題だけでなく、自然数やリストなどなど、普通のデータ型も、Inductiveで定義します。例えば自然数は Coq.Init.Datatypes.nat Inductive nat : Set := | O : nat | S : na…

Coqの入門記事を書く会 (3)

Coq

このペースだと、なかなかCoqの一番面白いところ(とわたしが思うところ)に行き着かないので、今回は全力ですっ飛ばして、必要な細かい話を全部片付けちゃおうと思います。次回が面白くなるはずです。今回は、主に、自然数やリストにまつわる証明の巻。

andとorとnot: 次回予告 (2.6)

Coq

もう今回の内容でInductiveの扱いは完璧…!といいたいところなんですが、「再帰的なInductive」の証明テクニックの解説が実はまだ残っています。次は多分それについて書きたいなあと思っています。それかFalse周りの証明をさらにいろいろ。

andとorとnot以外のInductive (2.5)

Coq

何度か繰り返しているように、andやorやFalseは、Coqに組み込みの摩訶不思議な何かではなく、ユーザー定義できる命題です。andやorに使える証明方法は、他のInductive命題にもそのまま使えます。試しに他に何か自作してみましょう。こんなの考えてみました。…

andとorとnot: デストラクト (2.4)

Coq

「コンストラクタがあるならデストラクタはないんですか」あるのです。これを語らなくては話が終わりません。コンストラクタの逆の話なので、例題も逆にしましょう。ド・モルガンの法則は逆向きにも成り立ちます。 Lemma De_Morgan2: forall A B: Prop, (~A …

andとorとnot: コンストラクタ (2.3)

Coq

ここまでの内容をまとめると、 ゴールが A∧B の形なら ∧の公理(コンストラクタ)を使う つまり apply conj. ゴールが A∨B の形なら ∨の公理(コンストラクタ)を使う つまり apply or_introl. または apply or_intror. どっちがいいかは人間が頑張って考える。 …

andとorとnot: カリーハワード (2.2)

Coq

「プログラミング言語としてみると」さっきの証明は何をやっていたことになるんでしょう。"Inductive"は、ユーザー定義の新しい命題を定義するのでした。そして、命題=型です。つまり、ユーザー定義の新しい型を作る機能が対応します。Haskell だと "data" …

andとorとnot: ド・モルガン (2.1)

Coq

andとorとnotを分けて説明するのが面倒くさいので、いきなり全部入りの定理を例にしましょう。今回のお題はド・モルガンの法則です。 Lemma De_Morgan: forall A B: Prop, ~(A \/ B) -> (~A /\ ~B). Proof.「(AまたはB)ではない、ならば、(Aではない、かつ、…

Coqの入門記事を書く会 (2)

Coq

第2回です。前回は「forall」と「->」の扱い方でした。今回は、「ならば (->)」以外の定番の論理演算、「and」「or」「not」のお話です。実は、Coq の本当に言語組み込みの命題構成子は forall と -> だけで、「and」「or」「not」は、Coq使いなら自分で同…

[Coq] forall と -> : まとめ (1.6)

というわけで、Coq入門編その一、forall と -> だけ使った定理の証明、をお届けしました。気が向いたら「and, or, not を使った定理の証明」「exists を使った定理の証明」「帰納法」「forallと->と依存型について本気出して考えてみた」… の順番で続きます…

forall と -> : 仮定側の変形 (1.5)

Coq

ここまでに紹介した apply と intro(s) は、どちらも、証明のゴールを変形する tactic でした。なのですが、これってあまり直感的ではない気がするのですよね。私見ですが。 「A と B と C を仮定して Z を証明して下さい!」 って言われたときに 「Cが使え…

forall と -> : ゴールが2つ (1.4)

Coq

別の例をやってみたいと思います。Sコンビネータと呼ばれる定理です。 Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R.いきなりexactで書いてもいいんですが、順を追ってやっていきましょう。 intros.「ゴールにforallや->があったら、と…

forall と -> : カリーハワード (1.3)

Coq

ところで、HaskellやOCamlなどの関数型言語をご存じの方なら100倍高速にCoqを理解できる!というショートカットのご紹介です。以下、この節限定で、説明にHaskellが混じります。Haskellわからんという人はこの節は飛ばしても以降に差し支えはない…はず…たぶ…

forall と -> (1.2)

Coq

いくつか細かい捕捉。introintrosと同じひっぺがし作業を1回だけやる単数形にすると「1回だけやる」意味になります。introsだとやれるまでやってしまうので、今回の例だと4個全部はがしちゃいますが Theorem Modus_ponens: forall (P: Prop), forall (Q: Pr…

forall と -> (1.1)

Coq

Modus Ponens 一番最初の例として Anarchy Proof 第1問: http://as305.dyndns.org/aps/problem/view/1 を証明してみよう。古代ギリシャから伝わる "Modus Ponens" とよばれる定理「"PならばQ" であり、しかも "P" ならば、それすなわち "Q" である」です。こ…

Coqの入門記事を書く会 (1)

Coq

証明支援系Coqの遊び方の入門を書いてみるよ。すでに世の中に何個も入門記事ありますけど、増えて困ることはなかろう…ということで。まず、インストール方法については、id:yoshihiro503 による紹介記事 http://d.hatena.ne.jp/yoshihiro503/20070706#p1 最…