X
トップページ⇒数学
274コメント91KB
【Coq】コンピューターで証明しよう【コック】©2ch.net
■ このスレッドは過去ログ倉庫に格納されています
0002片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/23(金) 01:51:30.31ID:kQ1pk3tS
自然数nに対する2n＝n＋nの証明の例。

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.
0003片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/23(金) 01:56:25.68ID:kQ1pk3tS
自然数nに対してn (n＋1)が偶数であることの証明の例。

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.
0004片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/23(金) 02:10:51.92ID:kQ1pk3tS
Coqは証明支援システムです。数学論文を英語で書ける程度の素養が必要です。
まずはTutorialを読むことから始めましょう。
natは自然数(natural numbers)の略です。
Coqでは英語や英語の略語がよく使われます。
0006１３２人目の素数さん
垢版 |
2015/01/23(金) 13:50:52.34ID:v4GbgrUP
　 　 　　　＿＿＿_
　 　　　／⌒　　⌒＼
　　　／ 　癶 　　癶　＼
　 ／::::::⌒（__人__）⌒::::: ＼　　　あらあらうふふ
　 |　　　　　|r┬-|　　　　　|
　 ＼ 　　 　 `ー'´ 　 　 ／
0008片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/23(金) 16:42:51.44ID:kQ1pk3tS
「Require Import Arith.」は、
「Arith」というモジュール(部品)を読み込むコマンドだ。
コマンド「Theorem t: forall n:nat, 2*n = n+n.」について。
「Theorem t:」は、これから「t」という名前の定理を証明するよって意味。
「forall n:nat,」は、「∀n∈Ｎ」という意味。
ここで「∀」は論理学における「任意の…に対して」という意味。
「∈」は集合論の「…に属する」に相当する。
0009片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/23(金) 16:48:37.07ID:kQ1pk3tS
掛け算について現在の定義を調べたいなら、掛け算の略は「mult」だから、「SearchAbout mult.」というコマンドを入力すればいい。
自然数について調べたいなら「SearchAbout nat.」を入力。
足し算なら「SearchAbout plus.」。
0010片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/23(金) 16:57:07.60ID:kQ1pk3tS
Theoremコマンドを入力したら、証明モードに入る。
証明モードでは、証明するための「タクティク」(戦術)を入力できる。
コマンドは大文字で始まるが、タクティクは小文字で始まる。
タクティクの例を挙げると、intros,symmetry,left,right,auto,elim,applyなど、いろんなタクティクがある。
証明の終わりでは「Qed.」コマンドを入力する。
0011片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/23(金) 17:12:06.01ID:kQ1pk3tS
さて、Coqのダウンロードとインストールが終わったら、早速Coqを起動しよう。
黒い画面に「Coq <」と表示されるだろう。
これはCoqのプロンプトであり、入力待ちであることを表している。
0012片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/23(金) 17:15:42.51ID:kQ1pk3tS
Coqの終了コマンドは「Quit.」である。「Quit.」と打ち込んでEnterキーを押せば
黒い画面が消えるであろう。
0013１３２人目の素数さん
垢版 |
2015/01/23(金) 21:55:31.77ID:bh227Vy0
suck my coq!
0015１３２人目の素数さん
垢版 |
2015/01/24(土) 00:15:52.39ID:G4KHuvpv
Coqは数学、プログラミング両方で高い水準を要求されるからな。
このスレは人集まらないだろう。
数板ではプログラムの素養がネックになるか？
0016１３２人目の素数さん
垢版 |
2015/01/24(土) 00:29:02.73ID:w9MHCKHx
証明支援系のプログラムにバグがないことはどうやって
証明するの？
0020１３２人目の素数さん
垢版 |
2015/01/24(土) 17:26:49.57ID:G4KHuvpv
-を+に変えた版はできた。
-の方はまだできてない。

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.
0022１３２人目の素数さん
垢版 |
2015/01/24(土) 22:01:32.97ID:WXgNhwIy
　　　　　　　 ／⌒ヽ⌒ヽ
　 　 　 　 　　 　 　 Ｙ
　　　　　　 　　　 　八　　ヽ
　　　　　（　　 __／/.　ヽ,, ,）
　　　　　 丶1　　　 八.　 !/
　　　　　　 ζ, 　　 八.　 j
　　　 　 　　i　　　 丿 ､　j
　　　　 　　 |　 　 　八 　 |
　　 　　　　 | !　　　 i　､　|
　　　　　　 | i し　"　i　 　'|
　　　　　　|ﾉ　(　　　i　 　 i|
　　　　　 (　'~ヽ　　　!　　‖
　 　 　 　 │　 　　　i　 　‖
　　　　　　|　　　　　　! 　 ||
　　　　　　|　　　 │　　　　|
　　 　　　|　 　 　 　| 　 　| |
　　　　　| 　 　　　　|　　　| |
　　　　 | 　　　　 　 !　　 　| |
0023１３２人目の素数さん
垢版 |
2015/01/25(日) 19:37:01.31ID:4ki3LVZe
Coq の論理的バックグラウンド（？）になってる
Calculus of Inductive Construction (CIC)
（？：何種類かあって良く分からない）
について調べたいのですが良い文献ないですか？
0025片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 16:34:55.90ID:SJxzPcnV
自然数の範囲では、>>18は証明できないよ。
整数か実数か複素数を使わないと。
0026片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 17:08:56.67ID:SJxzPcnV
Require Import Arith.
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.
0027片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 17:13:27.24ID:SJxzPcnV
Require Import Omega.
Open Scope Z_scope.
の後で
SearchAbout Z.するとZの定義が見られるからね。
0029片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 20:07:13.17ID:SJxzPcnV
>>26
訂正。ガラケーで入力大変。

(誤)
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.
0030片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 20:10:46.94ID:SJxzPcnV
お題：
「３の倍数に６を足したものは３の倍数である」を証明せよ。
0033片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 20:35:45.19ID:SJxzPcnV
>>30

「xは３の倍数である」
⇔
∃y∈Ｚに対して「x＝3y」、

だな。１階述語とexistsを使って解いてくれ。
0034片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 20:59:02.99ID:SJxzPcnV
例えば、
Definition trimul (n:nat) := exists m:nat, n = 3*m.
と定義すればtrimul(0)は次のように証明できる。
Theorem tmzero: trimul(0).
unfold trimul.
exists 0.
auto.
Qed.
0035片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 21:17:44.23ID:SJxzPcnV
>>30

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.
0036片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 21:25:18.31ID:SJxzPcnV
「Reset Initial.」コマンドでCoqを初期状態へ戻すことができる。
「unfold x.」はゴールにあるxをその定義に展開するタクティクだ。
「destruct H.」はHを崩すタクティク。
0039１３２人目の素数さん
垢版 |
2015/01/27(火) 21:52:51.06ID:BM4PDVdL
こう？

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.

多分このスレには片山さんと俺しかいないぞｗ
0040片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/27(火) 22:12:11.97ID:SJxzPcnV
>>39
正解！

このスレを立てた目的は…
１．Coqの知名度アップと啓蒙。
２．Coqによる「片山QZの定理」の証明。
３．Coqと人工知能の連携を考えること。
0042１３２人目の素数さん
垢版 |
2015/01/28(水) 18:28:09.93ID:Q7XfmRRj
どのお題も超簡単なものだけに見えるのだが、それはなぜ？
Coqでの証明法がだれにも分かりやすくなるようあえて題材は
簡単なものを選んでいるの？
もっとCoqの強力さが分かる位難しい題材でやってくれんかな。
そもそもCoqではどの位難しいものがどの位の手間で証明できるの？
0043片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/28(水) 18:52:58.11ID:xr03hxaD
>>41
単純に言えば、コンピューターでできた数学者を作ろうとしている。
数学の問題は、式の変形と問題の分解と解の探索の問題に還元されるから、
人工知能でもいくつかの問題を解くことができるはずだ。
0044片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/28(水) 18:58:35.37ID:xr03hxaD
>>42
はじめは基礎と慣れが大事。不満なら君も出題してもかまわない。
次は集合論から出題したまえ。
0048１３２人目の素数さん
垢版 |
2015/01/28(水) 20:07:20.02ID:Q7XfmRRj
>>44
集合問題でなく整数問題の系統だが、まずはこういう易しめのお題はどう？
お題：正整数m、nがあり、LCM(m,n) + GCD(m,n) = m + n とする。
このとき、m, n のどちらか一方は、他方によって割り切れることを示せ。
0050１３２人目の素数さん
垢版 |
2015/01/29(木) 09:57:12.57ID:rxXHbRm8
俺はCoqのド素人だから聞いてる。
だが人間にとって証明問題といえばふつうこれくらいからだろ？
0051１３２人目の素数さん
垢版 |
2015/01/30(金) 10:46:00.89ID:NnXyGTxc
☆☆☆☆☆
☆ 自民党、グッジョブですわ。 ☆
http://www.soumu.go.jp/senkyo/kokumin_touhyou/index.html

☆ 日本国民の皆様方、2016年7月の『第24回 参議院選挙』で、改憲の参議院議員が
3分の2以上を超えると日本国憲法の改正です。皆様方、必ず投票に自ら足を運んでください。
そして、私たちの日本国憲法を絶対に改正しましょう。☆
0053片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/01/31(土) 11:42:47.03ID:HFUS6FCH
>>48
http://ideone.com/Aa07zr

「Z.lcm m n = m0 * n0 * Z.gcd m n」の証明が難しい。
0057１３２人目の素数さん
垢版 |
2015/01/31(土) 14:08:26.29ID:2+EKWeFU
>>53
まじめにやってくれてサンクス。
それで
>http://ideone.com/Aa07zr
これはすべて人が書いてるんだね？　だとするとメリットがわからんな。
「コンピュータを使って定理証明する」て、人が形式証明を計算機に打ち込む
ということか？ふつうはそれとは違う意味で言うことだが。
0062片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/02/01(日) 23:27:39.12ID:/+/CiuQP
>>46ができたヤツは居ないか？
0063１３２人目の素数さん
垢版 |
2015/02/02(月) 20:07:15.55ID:yNmPHm6y
>>46チャレンジしようとして集合のモジュール名がわからなくて投げた俺が通りますよ。
0066１３２人目の素数さん
垢版 |
2015/02/02(月) 21:41:32.43ID:yNmPHm6y
stdlib読んでも意味わかんなかった俺が通りますよｗ
Ensemblesってのでいいのか？
そこからわからんｗ
0067１３２人目の素数さん
垢版 |
2015/02/02(月) 22:26:56.55ID:yNmPHm6y
じっくり読むとなんとなくわかってくるな。
もうちょっとやってみるわ
0070１３２人目の素数さん
垢版 |
2015/02/03(火) 06:21:09.41ID:AsZmhMLH
(・ω・)
0071１３２人目の素数さん
垢版 |
2015/02/03(火) 11:39:09.23ID:TF0+kICu
>>69
賛成かな？　
ただ俺の場合は、Coqの細かい話はうんざりだ。単なる証明支援の今のCoqなら将来はないんだから。
早く自動証明の話をしてくれ
0072片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/02/03(火) 17:56:27.70ID:lc3NHdIs
Coq自体は、関数型言語として有名なOCamlで記述されている。
Coqのソースコードは同じ場所でダウンロードできる。
自動証明を行いたいなら、Omegaのようなモジュールを自作するか、
Coqを改造するか、Coqと対話する必要がある。
0073片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/02/03(火) 18:12:57.83ID:lc3NHdIs
最新のソースコードcoq-8.4pl5.tar.gzをダウンロードし、解凍ソフトLhaplusなどを使って解凍(展開)すると、
coq-8.4pl5というフォルダーができる。
ここにパスcoq-8.4pl5/plugins/omega/にOmegaが記述されている。
ファイルの中身はテキストエディターなどで確認できる。
0075１３２人目の素数さん
垢版 |
2015/02/04(水) 10:08:30.01ID:cf1lNhgP
> 自動証明を行いたいなら、Omegaのようなモジュールを自作するか、
> Coqを改造するか、Coqと対話する必要がある。
Coqの延長でできる風に言ってるが、それはもうCoqではないだろう
0076１３２人目の素数さん
垢版 |
2015/02/04(水) 12:44:57.04ID:ii+fPoPp
人工知能の進歩を見てると、やはり半端ない多量の証明のデータの蓄積をした上で、それをコンピュータ自身が分析し、与えられた定理にはどのような手法が適している可能性が高いかを推測するようなシステムになるのかな。
人間も結局過去の膨大な証明から経験的に学んでるわけだし。
0078１３２人目の素数さん
垢版 |
2015/02/04(水) 21:09:33.67ID:ZZSly8gS
Coqが証明できる定理ってなにか制限あるの？
それとも人間が証明できる定理は原理的にCoqでも証明できる？
0081１３２人目の素数さん
垢版 |
2015/02/05(木) 19:10:49.09ID:iuUfy0y0
コンパイラも文法チェックはするが、コンパイラがプログラミングしてるとは言わんだろ
0083１３２人目の素数さん
垢版 |
2015/02/05(木) 19:29:39.63ID:160T3VWS
ランダム生成やってみれば
0084１３２人目の素数さん
垢版 |
2015/02/05(木) 19:53:49.21ID:RkehamlL
メモリいっぱい積んで幅優先でやってみたいね。
すぐメモリたんなくなるだろうけど。
0085１３２人目の素数さん
垢版 |
2015/02/05(木) 20:23:32.85ID:iuUfy0y0
>>82
一苦労どころじゃないだろｗ
このスレッドを見ても、ほとんど定義そのもの程度の命題の証明がお題になるくらいだからな
0086１３２人目の素数さん
垢版 |
2015/02/06(金) 10:38:19.60ID:p5z+W0p1
CICのnormalization theoremを証明してあるわかりやすい文献教えてくらはい、えらいひと。
0087片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/02/08(日) 17:07:42.20ID:6NKOGxqa
お題：中国剰余定理を証明せよ。
0094１３２人目の素数さん
垢版 |
2015/02/10(火) 21:31:54.68ID:HSrgtPR2
個人でいきなり読みにいってもきっと読めないんでしょ？
数学の本スレでちょっと前に誰かが聞いて、
経験者らしきそっちの学識ありそうな誰かが応えてた
自動定理証明器の古典本あたりから読まないと・・・

勉強会とかするなら参加したいわ
0095片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/02/11(水) 07:12:51.62ID:Dr+1DDR1
数学の体系は、公理系によって成り立っている。すなわち、
当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、
さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。
そのように数学は、間違いのない証明によって次々と築き上げるものである。
0096片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/02/11(水) 07:20:21.76ID:Dr+1DDR1
証明に１つでも間違いがあれば、公理系は崩壊する。間違いが１つでも紛れ込めば、
どんな命題でも証明可能になり、証明が無意味となる。
■ このスレッドは過去ログ倉庫に格納されています
ニューススポーツなんでも実況