15/01/27 20:27:34.17 SJxzPcnV
>>24
聞いた覚えはないな
34:片山博文MZ ◆T6xkBnTXz7B0
15/01/27 20:35:45.19 SJxzPcnV
>>30
「xは３の倍数である」
⇔
∃y∈Ｚに対して「x＝3y」、
だな。１階述語とexistsを使って解いてくれ。
35:片山博文MZ ◆T6xkBnTXz7B0
15/01/27 20:59:02.99 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
15/01/27 21:17:44.23 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
15/01/27 21:25:18.31 SJxzPcnV
「Reset Initial.」コマンドでCoqを初期状態へ戻すことができる。
「unfold x.」はゴールにあるxをその定義に展開するタクティクだ。
「destruct H.」はHを崩すタクティク。
38:片山博文MZ ◆T6xkBnTXz7B0
15/01/27 21:30:41.25 SJxzPcnV
お題：
「３の倍数に４を掛けたものは６の倍数である」を証明。
39:１３２人目の素数さん
15/01/27 21:32:30.82 BM4PDVdL
片山さん結構勉強進んでるな。
40:１３２人目の素数さん
15/01/27 21:52:51.06 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
15/01/27 22:12:11.97 SJxzPcnV
>>39
正解！
このスレを立てた目的は…
１．Coqの知名度アップと啓蒙。
２．Coqによる「片山QZの定理」の証明。
３．Coqと人工知能の連携を考えること。
42:１３２人目の素数さん
15/01/28 08:18:03.12 Q7XfmRRj
>３．Coqと人工知能の連携を考えること。
ここをもう少し詳しく
43:１３２人目の素数さん
15/01/28 18:28:09.93 Q7XfmRRj
どのお題も超簡単なものだけに見えるのだが、それはなぜ？
Coqでの証明法がだれにも分かりやすくなるようあえて題材は
簡単なものを選んでいるの？
もっとCoqの強力さが分かる位難しい題材でやってくれんかな。
そもそもCoqではどの位難しいものがどの位の手間で証明できるの？
44:片山博文MZ ◆T6xkBnTXz7B0
15/01/28 18:52:58.11 xr03hxaD
>>41
単純に言えば、コンピューターでできた数学者を作ろうとしている。
数学の問題は、式の変形と問題の分解と解の探索の問題に還元されるから、
人工知能でもいくつかの問題を解くことができるはずだ。
45:片山博文MZ ◆T6xkBnTXz7B0
15/01/28 18:58:35.37 xr03hxaD
>>42
はじめは基礎と慣れが大事。不満なら君も出題してもかまわない。
次は集合論から出題したまえ。
46:１３２人目の素数さん
15/01/28 19:12:43.24 MQBQj2T8
>>44
なぜ集合論？
一応念のためいっとくが>>42は某スレの1(俺)とは別人だぞ。
47:片山博文MZ ◆T6xkBnTXz7B0
15/01/28 19:42:58.51 xr03hxaD
お題：
「Z⊆XかつZ⊆YならばZ⊆X∩Y」を証明せよ。
48:１３２人目の素数さん
15/01/28 20:04:26.42 Q7XfmRRj
>>43
Coqあるいは片山さんは、東大ロボプロジェクトはどう評価してるの？
49:１３２人目の素数さん
15/01/28 20:07:20.02 Q7XfmRRj
>>44
集合問題でなく整数問題の系統だが、まずはこういう易しめのお題はどう？
お題：正整数m、nがあり、LCM(m,n) + GCD(m,n) = m + n とする。
このとき、m, n のどちらか一方は、他方によって割り切れることを示せ。
50:１３２人目の素数さん
15/01/28 22:31:29.58 MQBQj2T8
易しいっていうけど>>48は>>48の証明をCoqでできるの？
51:１３２人目の素数さん
15/01/29 09:57:12.57 rxXHbRm8
俺はCoqのド素人だから聞いてる。
だが人間にとって証明問題といえばふつうこれくらいからだろ？
52:１３２人目の素数さん
15/01/30 10:46:00.89 NnXyGTxc
☆☆☆☆☆
☆ 自民党、グッジョブですわ。 ☆
URLﾘﾝｸ(www.soumu.go.jp)
☆ 日本国民の皆様方、2016年7月の『第24回 参議院選挙』で、改憲の参議院議員が
3分の2以上を超えると日本国憲法の改正です。皆様方、必ず投票に自ら足を運んでください。
そして、私たちの日本国憲法を絶対に改正しましょう。☆
53:１３２人目の素数さん
15/01/30 11:16:04.23 UCtzINaz
>>23