ひとり勉強会

ひとり楽しく勉強会

2010-09-19から1日間の記事一覧

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