【Coq】コンピューターで証明しよう【コック】
http://www.iij-ii.co.jp/lab/techdoc/coqt/
http://ja.wikipedia.org/wiki/Coq
使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。
さあ、試してみよう！
Require Import Arith.
Theorem t: forall n:nat, 2*n = n+n.
intros.
replace (n+n) with (1*n + 1*n).
replace 2 with (1+1).
apply mult_plus_distr_r.
auto.
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
Qed.
Require Import Even.
Theorem t:forall n:nat, even (n * (1+n)).
intros.
apply even_mult_aux.
elim n.
left.
apply even_O.
intros.
elim H.
right.
apply even_S.
apply odd_S.
apply H0.
left.
apply H0.
Qed.
まずはTutorialを読むことから始めましょう。
natは自然数(natural numbers)の略です。
Coqでは英語や英語の略語がよく使われます。
そこんとこ誤解させんなよ
／⌒ ⌒＼
／ 癶 癶 ＼
／::::::⌒（__人__）⌒::::: ＼ あらあらうふふ
| |r┬-| |
＼ `ー'´ ／
すみません。
>>6
English speakerに前置きなく「コック」って言ったら誤解を産むよね。
「Arith」というモジュール(部品)を読み込むコマンドだ。
コマンド「Theorem t: forall n:nat, 2*n = n+n.」について。
「Theorem t:」は、これから「t」という名前の定理を証明するよって意味。
「forall n:nat,」は、「∀n∈Ｎ」という意味。
ここで「∀」は論理学における「任意の…に対して」という意味。
「∈」は集合論の「…に属する」に相当する。
自然数について調べたいなら「SearchAbout nat.」を入力。
足し算なら「SearchAbout plus.」。
証明モードでは、証明するための「タクティク」(戦術)を入力できる。
コマンドは大文字で始まるが、タクティクは小文字で始まる。
タクティクの例を挙げると、intros,symmetry,left,right,auto,elim,applyなど、いろんなタクティクがある。
証明の終わりでは「Qed.」コマンドを入力する。
黒い画面に「Coq <」と表示されるだろう。
これはCoqのプロンプトであり、入力待ちであることを表している。
黒い画面が消えるであろう。
このスレは人集まらないだろう。
数板ではプログラムの素養がネックになるか？
証明するの？
x^2 - 2x + 1 ＝ (x - 1)^2の証明。
いやいや、いいスレだ。せいぜい集まろうぜ
-の方はまだできてない。
Require Import Omega.
Require Import Arith.
Theorem t:forall n:nat,n*n+2*n+1=(n+1)*(n+1).
intros.
replace (2*n) with (n+n).
symmetry.
replace ((n+1)*(n+1)) with (n*(n+1)+1*(n+1)).
replace (n*(n+1)) with (n*n+n*1).
omega.
symmetry.
apply mult_plus_distr_l.
symmetry.
apply mult_plus_distr_r.
omega.
Qed.
もう少しだな。-2x＝+(-2)xを使えば、できるはずだ。
Ｙ
八 ヽ
（ __／/. ヽ,, ,）
丶1 八. !/
ζ, 八. j
i 丿 ､ j
| 八 |
| ! i ､ |
| i し " i '|
|ﾉ ( i i|
( '~ヽ ! ‖
│ i ‖
| ! ||
| │ |
| | | |
| | | |
| ! | |
Calculus of Inductive Construction (CIC)
（？：何種類かあって良く分からない）
について調べたいのですが良い文献ないですか？
整数か実数か複素数を使わないと。
Require Import Omega.
Open Scope Z_scope.
Theorem t: forall n:Z, n*n - 2*n + 1 = (n-1)*(n-1).
intros.
symmetry.
replace ((n-1)*(n-1)) with (n*(n-1)-1*(n-1)).
replace (1*(n-1)) with (n-1).
replace (n*(n-1)) with (n*n-n).
replace (n*n-n-(n-1)) with (n*n-(n-1)-n).
replace (n*n-(n-1)) with (n*n-n+1).
replace (n*n-n+1-n) with (n*n-n-n+1).
replace (n*n-n-n) with (n*n-2*n).
omega.
omega.
omega.
omega.
omega.
symmetry.
replace (n*n-n) with (n*n-n*1).
apply Z.mul_sub_distr_l.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.
Open Scope Z_scope.
の後で
SearchAbout Z.するとZの定義が見られるからね。
俺の環境だと証明が通らないんだが。
なんかミスってない？
訂正。ガラケーで入力大変。
(誤)
apply Z.mul_sub_distr_l.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.
(正)
apply Z.mul_sub_distr_l.
omega.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.
「３の倍数に６を足したものは３の倍数である」を証明せよ。
通った。
聞いた覚えはないな
「xは３の倍数である」
⇔
∃y∈Ｚに対して「x＝3y」、
だな。１階述語とexistsを使って解いてくれ。
Definition trimul (n:nat) := exists m:nat, n = 3*m.
と定義すればtrimul(0)は次のように証明できる。
Theorem tmzero: trimul(0).
unfold trimul.
exists 0.
auto.
Qed.
Require Import Arith.
Require Import Omega.
Open Scope Z_scope.
Definition trimul (x:Z) := exists y:Z, x = 3*y.
Theorem t: forall x:Z, trimul(x) -> trimul(x+6).
intros.
unfold trimul.
destruct H.
exists (x0+2).
replace (x) with (3*x0).
omega.
Qed.
「unfold x.」はゴールにあるxをその定義に展開するタクティクだ。
「destruct H.」はHを崩すタクティク。
「３の倍数に４を掛けたものは６の倍数である」を証明。
Require Import Omega.
Require Import Arith.
Open Scope Z_scope.
Definition tr(x:Z) := exists y:Z , x=3*y.
Definition s(x:Z) := exists y:Z,x=6*y.
Theorem t: forall x:Z,tr(x)->s(4*x).
intros.
unfold s.
destruct H.
exists (2*x0).
replace x with (3*x0).
omega.
Qed.
多分このスレには片山さんと俺しかいないぞｗ
正解！
このスレを立てた目的は…
１．Coqの知名度アップと啓蒙。
２．Coqによる「片山QZの定理」の証明。
３．Coqと人工知能の連携を考えること。
ここをもう少し詳しく
Coqでの証明法がだれにも分かりやすくなるようあえて題材は
簡単なものを選んでいるの？
もっとCoqの強力さが分かる位難しい題材でやってくれんかな。
そもそもCoqではどの位難しいものがどの位の手間で証明できるの？
単純に言えば、コンピューターでできた数学者を作ろうとしている。
数学の問題は、式の変形と問題の分解と解の探索の問題に還元されるから、
人工知能でもいくつかの問題を解くことができるはずだ。
はじめは基礎と慣れが大事。不満なら君も出題してもかまわない。
次は集合論から出題したまえ。
なぜ集合論？
一応念のためいっとくが>>42は某スレの1(俺)とは別人だぞ。
「Z⊆XかつZ⊆YならばZ⊆X∩Y」を証明せよ。
Coqあるいは片山さんは、東大ロボプロジェクトはどう評価してるの？
集合問題でなく整数問題の系統だが、まずはこういう易しめのお題はどう？
お題：正整数m、nがあり、LCM(m,n) + GCD(m,n) = m + n とする。
このとき、m, n のどちらか一方は、他方によって割り切れることを示せ。
だが人間にとって証明問題といえばふつうこれくらいからだろ？
☆ 自民党、グッジョブですわ。 ☆
http://www.soumu.go.jp/senkyo/kokumin_touhyou/index.html
☆ 日本国民の皆様方、2016年7月の『第24回 参議院選挙』で、改憲の参議院議員が
3分の2以上を超えると日本国憲法の改正です。皆様方、必ず投票に自ら足を運んでください。
そして、私たちの日本国憲法を絶対に改正しましょう。☆
http://ideone.com/Aa07zr
「Z.lcm m n = m0 * n0 * Z.gcd m n」の証明が難しい。
名古屋大学 佐藤雅大さん
http://shirodanuki.cs.shinshu-u.ac.jp/TPP/TPP2013_satou.pdf
からTutorial.pdfとReference-Manual.pdfとrefman.tar.gzを
ダウンロードすること。
まじめにやってくれてサンクス。
それで
>http://ideone.com/Aa07zr
これはすべて人が書いてるんだね？ だとするとメリットがわからんな。
「コンピュータを使って定理証明する」て、人が形式証明を計算機に打ち込む
ということか？ふつうはそれとは違う意味で言うことだが。
それは私が書きました。
Classicalモジュールを使えばね
東大ロボは>>48くらいは当然自動で解くんだがね
Ensemblesってのでいいのか？
そこからわからんｗ
もうちょっとやってみるわ
よくわからぬ。
自動定理証明器の設計の話題にまで広がりますように
賛成かな？
ただ俺の場合は、Coqの細かい話はうんざりだ。単なる証明支援の今のCoqなら将来はないんだから。
早く自動証明の話をしてくれ
Coqのソースコードは同じ場所でダウンロードできる。
自動証明を行いたいなら、Omegaのようなモジュールを自作するか、
Coqを改造するか、Coqと対話する必要がある。
coq-8.4pl5というフォルダーができる。
ここにパスcoq-8.4pl5/plugins/omega/にOmegaが記述されている。
ファイルの中身はテキストエディターなどで確認できる。
Coqスレ
http://peace.2ch.sc/test/read.cgi/tech/1300017923/
> Coqを改造するか、Coqと対話する必要がある。
Coqの延長でできる風に言ってるが、それはもうCoqではないだろう
人間も結局過去の膨大な証明から経験的に学んでるわけだし。
それとも人間が証明できる定理は原理的にCoqでも証明できる？
Coqはなにも証明しない！人間が証明してる。Coqは証明用ワープロ
えっ、正しい論証になってるかチェックしてくれないの？
すぐメモリたんなくなるだろうけど。
一苦労どころじゃないだろｗ
このスレッドを見ても、ほとんど定義そのもの程度の命題の証明がお題になるくらいだからな
OCamlな。
Coqの動作原理を知りたいならOCamlで書かれたCoqのソースとにらめっこ
心臓部を理解すれば後は枝葉
心臓部とか何ステップくらいなのよ？
数学の本スレでちょっと前に誰かが聞いて、
経験者らしきそっちの学識ありそうな誰かが応えてた
自動定理証明器の古典本あたりから読まないと・・・
勉強会とかするなら参加したいわ
当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、
さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。
そのように数学は、間違いのない証明によって次々と築き上げるものである。
どんな命題でも証明可能になり、証明が無意味となる。
なにを言いたい？
なお、証明が間違っていても公理系は崩壊しないｗ
この船頭では…
公理の集合のことを公理系って言うんだったね。
よって>>95-96は間違い。
100〜のスレッドの続きを読む
