- 1 名前：片山博文MZ ◆T6xkBnTXz7B0 転載ダメ©2ch.net mailto:sageteoff [2015/01/23(金) 01:41:03.17 ID:kQ1pk3tS]
- Coqというプログラムを使えば、計算機上で数学的な証明を厳密に行うことができます。
www.iij-ii.co.jp/lab/techdoc/coqt/
ja.wikipedia.org/wiki/Coq
使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。
さあ、試してみよう！
- 23 名前：１３２人目の素数さん mailto:sage [2015/01/24(土) 22:01:32.97 ID:WXgNhwIy]
- ／⌒ヽ⌒ヽ
Ｙ
八 ヽ
（ __／/. ヽ,, ,）
丶1 八. !/
ζ, 八. j
i 丿 ､ j
| 八 |
| ! i ､ |
| i し " i '|
|ﾉ ( i i|
( '~ヽ ! ‖
│ i ‖
| ! ||
| │ |
| | | |
| | | |
| ! | |
- 24 名前：１３２人目の素数さん mailto:sage [2015/01/25(日) 19:37:01.31 ID:4ki3LVZe]
- Coq の論理的バックグラウンド（？）になってる
Calculus of Inductive Construction (CIC)
（？：何種類かあって良く分からない）
について調べたいのですが良い文献ないですか？
- 25 名前：１３２人目の素数さん mailto:っｄ [2015/01/25(日) 19:45:30.26 ID:HYD7R+Gz]
- 仕様記述言語Zとの関聯はないの？
- 26 名前：片山博文MZ ◆T6xkBnTXz7B0 [2015/01/27(火) 16:34:55.90 ID:SJxzPcnV]
- 自然数の範囲では、>>18は証明できないよ。
整数か実数か複素数を使わないと。
- 27 名前：片山博文MZ ◆T6xkBnTXz7B0 [2015/01/27(火) 17:08:56.67 ID: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.
- 28 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 17:13:27.24 ID:SJxzPcnV]
- Require Import Omega.
Open Scope Z_scope.
の後で
SearchAbout Z.するとZの定義が見られるからね。
- 29 名前：１３２人目の素数さん mailto:sage [2015/01/27(火) 19:50:17.70 ID:BM4PDVdL]
- >>26
俺の環境だと証明が通らないんだが。
なんかミスってない？
- 30 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 20:07:13.17 ID: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.
- 31 名前：片山博文MZ ◆T6xkBnTXz7B0 [2015/01/27(火) 20:10:46.94 ID:SJxzPcnV]
- お題：
「３の倍数に６を足したものは３の倍数である」を証明せよ。
- 32 名前：１３２人目の素数さん mailto:sage [2015/01/27(火) 20:19:16.49 ID:BM4PDVdL]
- >>29
通った。
- 33 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 20:27:34.17 ID:SJxzPcnV]
- >>24
聞いた覚えはないな
- 34 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 20:35:45.19 ID:SJxzPcnV]
- >>30
「xは３の倍数である」
⇔
∃y∈Ｚに対して「x＝3y」、
だな。１階述語とexistsを使って解いてくれ。
- 35 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 20:59:02.99 ID:SJxzPcnV]
- 例えば、
Definition trimul (n:nat) := exists m:nat, n = 3*m.
と定義すればtrimul(0)は次のように証明できる。
Theorem tmzero: trimul(0).
unfold trimul.
exists 0.
auto.
Qed.
- 36 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 21:17:44.23 ID: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.
- 37 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 21:25:18.31 ID:SJxzPcnV]
- 「Reset Initial.」コマンドでCoqを初期状態へ戻すことができる。
「unfold x.」はゴールにあるxをその定義に展開するタクティクだ。
「destruct H.」はHを崩すタクティク。
- 38 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 21:30:41.25 ID:SJxzPcnV]
- お題：
「３の倍数に４を掛けたものは６の倍数である」を証明。
- 39 名前：１３２人目の素数さん mailto:sage [2015/01/27(火) 21:32:30.82 ID:BM4PDVdL]
- 片山さん結構勉強進んでるな。
- 40 名前：１３２人目の素数さん mailto:sage [2015/01/27(火) 21:52:51.06 ID: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.
多分このスレには片山さんと俺しかいないぞｗ
- 41 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/27(火) 22:12:11.97 ID:SJxzPcnV]
- >>39
正解！
このスレを立てた目的は…
１．Coqの知名度アップと啓蒙。
２．Coqによる「片山QZの定理」の証明。
３．Coqと人工知能の連携を考えること。
- 42 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 08:18:03.12 ID:Q7XfmRRj]
- >３．Coqと人工知能の連携を考えること。
ここをもう少し詳しく
- 43 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 18:28:09.93 ID:Q7XfmRRj]
- どのお題も超簡単なものだけに見えるのだが、それはなぜ？
Coqでの証明法がだれにも分かりやすくなるようあえて題材は
簡単なものを選んでいるの？
もっとCoqの強力さが分かる位難しい題材でやってくれんかな。
そもそもCoqではどの位難しいものがどの位の手間で証明できるの？
- 44 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/28(水) 18:52:58.11 ID:xr03hxaD]
- >>41
単純に言えば、コンピューターでできた数学者を作ろうとしている。
数学の問題は、式の変形と問題の分解と解の探索の問題に還元されるから、
人工知能でもいくつかの問題を解くことができるはずだ。
- 45 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/28(水) 18:58:35.37 ID:xr03hxaD]
- >>42
はじめは基礎と慣れが大事。不満なら君も出題してもかまわない。
次は集合論から出題したまえ。
- 46 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 19:12:43.24 ID:MQBQj2T8]
- >>44
なぜ集合論？
一応念のためいっとくが>>42は某スレの1(俺)とは別人だぞ。
- 47 名前：片山博文MZ ◆T6xkBnTXz7B0 mailto:sage [2015/01/28(水) 19:42:58.51 ID:xr03hxaD]
- お題：
「Z⊆XかつZ⊆YならばZ⊆X∩Y」を証明せよ。
- 48 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 20:04:26.42 ID:Q7XfmRRj]
- >>43
Coqあるいは片山さんは、東大ロボプロジェクトはどう評価してるの？
- 49 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 20:07:20.02 ID:Q7XfmRRj]
- >>44
集合問題でなく整数問題の系統だが、まずはこういう易しめのお題はどう？
お題：正整数m、nがあり、LCM(m,n) + GCD(m,n) = m + n とする。
このとき、m, n のどちらか一方は、他方によって割り切れることを示せ。
- 50 名前：１３２人目の素数さん mailto:sage [2015/01/28(水) 22:31:29.58 ID:MQBQj2T8]
- 易しいっていうけど>>48は>>48の証明をCoqでできるの？
- 51 名前：１３２人目の素数さん mailto:sage [2015/01/29(木) 09:57:12.57 ID:rxXHbRm8]
- 俺はCoqのド素人だから聞いてる。
だが人間にとって証明問題といえばふつうこれくらいからだろ？
- 52 名前：１３２人目の素数さん [2015/01/30(金) 10:46:00.89 ID:NnXyGTxc]
- ☆☆☆☆☆
☆ 自民党、グッジョブですわ。 ☆
www.soumu.go.jp/senkyo/kokumin_touhyou/index.html
☆ 日本国民の皆様方、2016年7月の『第24回 参議院選挙』で、改憲の参議院議員が
3分の2以上を超えると日本国憲法の改正です。皆様方、必ず投票に自ら足を運んでください。
そして、私たちの日本国憲法を絶対に改正しましょう。☆
- 53 名前：１３２人目の素数さん mailto:sage [2015/01/30(金) 11:16:04.23 ID:UCtzINaz]
- >>23
|
 |
