2010-09-01から1ヶ月間の記事一覧
駆け足でいろいろ紹介しました。 SearchAbout でライブラリを検索 自然数やリストはInductiveなデータ = に関する証明 reflexivity, symmetry, transitivity, discriminate = を使った書き換え rewrite, replace 計算をすすめる simpl, cbv, ... 自動証明 om…
ここまで forall, ->, and, or, not のCoqでの使い方を見ました。Wikipediaの一階述語論理のページなどを見てみると、もう一種類、この手の論理結合子があります。∃(存在する)。Coq では、exists と書きます。 Theorem even_or_odd: forall (n:nat), exist…
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こう右下に表示されると思…
別の問題を証明してみましょう。Anarchy Proof から Sum of natural numbers をお借りします。ring を使わないでやってみよう、という問題ですが、気にせずringを使って解いちゃいますので、ネタバレにはなっていないはず…。 Require Import Arith Omega. Fi…
Coqさんは非常に賢いので、実は、今回くらいの証明は自動でやってくれます。 Proof. intros. omega. Qed.omega はプレスバーガー算術という美味しそうな名前の理論の簡易全自動ソルバーで、整数に関する等式や不等式のかなりの部分を自動的に証明してくれま…
x=0の場合は終わったので、残ったゴールはこれです。 ------------------------- S x < S x + S xこれを証明するには…なにか、このくらいはさっきImportしたArith標準ライブラリで証明されていないでしょうか。CoqIDEでは SearchAbout (_ < _ + _).と打ち込…
前回、andやorなどの命題が"Inductive"で作られてることをご紹介しました。Coqでは、命題だけでなく、自然数やリストなどなど、普通のデータ型も、Inductiveで定義します。例えば自然数は Coq.Init.Datatypes.nat Inductive nat : Set := | O : nat | S : na…
このペースだと、なかなかCoqの一番面白いところ(とわたしが思うところ)に行き着かないので、今回は全力ですっ飛ばして、必要な細かい話を全部片付けちゃおうと思います。次回が面白くなるはずです。今回は、主に、自然数やリストにまつわる証明の巻。
もう今回の内容でInductiveの扱いは完璧…!といいたいところなんですが、「再帰的なInductive」の証明テクニックの解説が実はまだ残っています。次は多分それについて書きたいなあと思っています。それかFalse周りの証明をさらにいろいろ。
何度か繰り返しているように、andやorやFalseは、Coqに組み込みの摩訶不思議な何かではなく、ユーザー定義できる命題です。andやorに使える証明方法は、他のInductive命題にもそのまま使えます。試しに他に何か自作してみましょう。こんなの考えてみました。…
「コンストラクタがあるならデストラクタはないんですか」あるのです。これを語らなくては話が終わりません。コンストラクタの逆の話なので、例題も逆にしましょう。ド・モルガンの法則は逆向きにも成り立ちます。 Lemma De_Morgan2: forall A B: Prop, (~A …
ここまでの内容をまとめると、 ゴールが A∧B の形なら ∧の公理(コンストラクタ)を使う つまり apply conj. ゴールが A∨B の形なら ∨の公理(コンストラクタ)を使う つまり apply or_introl. または apply or_intror. どっちがいいかは人間が頑張って考える。 …
「プログラミング言語としてみると」さっきの証明は何をやっていたことになるんでしょう。"Inductive"は、ユーザー定義の新しい命題を定義するのでした。そして、命題=型です。つまり、ユーザー定義の新しい型を作る機能が対応します。Haskell だと "data" …
andとorとnotを分けて説明するのが面倒くさいので、いきなり全部入りの定理を例にしましょう。今回のお題はド・モルガンの法則です。 Lemma De_Morgan: forall A B: Prop, ~(A \/ B) -> (~A /\ ~B). Proof.「(AまたはB)ではない、ならば、(Aではない、かつ、…
第2回です。前回は「forall」と「->」の扱い方でした。今回は、「ならば (->)」以外の定番の論理演算、「and」「or」「not」のお話です。実は、Coq の本当に言語組み込みの命題構成子は forall と -> だけで、「and」「or」「not」は、Coq使いなら自分で同…
というわけで、Coq入門編その一、forall と -> だけ使った定理の証明、をお届けしました。気が向いたら「and, or, not を使った定理の証明」「exists を使った定理の証明」「帰納法」「forallと->と依存型について本気出して考えてみた」… の順番で続きます…
ここまでに紹介した apply と intro(s) は、どちらも、証明のゴールを変形する tactic でした。なのですが、これってあまり直感的ではない気がするのですよね。私見ですが。 「A と B と C を仮定して Z を証明して下さい!」 って言われたときに 「Cが使え…
別の例をやってみたいと思います。Sコンビネータと呼ばれる定理です。 Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R.いきなりexactで書いてもいいんですが、順を追ってやっていきましょう。 intros.「ゴールにforallや->があったら、と…
ところで、HaskellやOCamlなどの関数型言語をご存じの方なら100倍高速にCoqを理解できる!というショートカットのご紹介です。以下、この節限定で、説明にHaskellが混じります。Haskellわからんという人はこの節は飛ばしても以降に差し支えはない…はず…たぶ…
いくつか細かい捕捉。introintrosと同じひっぺがし作業を1回だけやる単数形にすると「1回だけやる」意味になります。introsだとやれるまでやってしまうので、今回の例だと4個全部はがしちゃいますが Theorem Modus_ponens: forall (P: Prop), forall (Q: Pr…
Modus Ponens 一番最初の例として Anarchy Proof 第1問: http://as305.dyndns.org/aps/problem/view/1 を証明してみよう。古代ギリシャから伝わる "Modus Ponens" とよばれる定理「"PならばQ" であり、しかも "P" ならば、それすなわち "Q" である」です。こ…
証明支援系Coqの遊び方の入門を書いてみるよ。すでに世の中に何個も入門記事ありますけど、増えて困ることはなかろう…ということで。まず、インストール方法については、id:yoshihiro503 による紹介記事 http://d.hatena.ne.jp/yoshihiro503/20070706#p1 最…