X
トップページ⇒数学
274コメント91KB

【Coq】コンピューターで証明しよう【コック】©2ch.net

■ このスレッドは過去ログ倉庫に格納されています
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
証明に１つでも間違いがあれば、公理系は崩壊する。間違いが１つでも紛れ込めば、
どんな命題でも証明可能になり、証明が無意味となる。
0104片山博文MZ ◆T6xkBnTXz7B0
垢版 |
2015/02/13(金) 02:36:25.72ID:4T+ZQiA6
同値変換だけで命題論理式を最も単純な節形式にするって未解決だよな？
0108１３２人目の素数さん
垢版 |
2015/02/16(月) 06:52:55.96ID:eGQOGV7p
私、O'Camlなどでのプログラミング経験はあるが数学の力に自信がないもので、数学書を一人で読み進める時にきちんと証明出来ている確信が欲しくて久しぶりにCoqを触り始めました。
証明のコードを生成してみるのもまた愉し。
0112１３２人目の素数さん
垢版 |
2015/03/17(火) 11:09:06.79ID:p3znTvh+
検証と証明ってどう違うの
一例の場合か全ての場合かってこと？
0113１３２人目の素数さん
垢版 |
2015/03/17(火) 12:42:17.91ID:SwDWqZM9
具体的に人間が与えた証明が正しい推論になっているか確かめるのが検証。
証明システムなら人工知能が結論までの道筋を自ら見つけるということになるはず。
0115１３２人目の素数さん
垢版 |
2015/03/19(木) 15:02:35.75ID:g9YALw9l
Variable A:Type.
Variable B:(A -> Type) -> A -> Type.
Definition mu := fun (x:A) => forall P:(A -> Type), (forall (y:A), B P y -> P y) -> P x.
Hypothesis m : forall (P Q:A -> Type), (forall (x:A), P x -> Q x) -> (forall (x:A), B P x -> B Q x).
での
Theorem r1:forall (x:A), B mu x -> mu x.
の証明なんだけど、
2 subgoals
A : Type
B : (A -> Type) -> A -> Type
m : forall P Q : A -> Type,
(forall x : A, P x -> Q x) -> forall x : A, B P x -> B Q x
x : A
a : B mu x
P : A -> Type
b : forall y : A, B P y -> P y
x0 : A
y : mu x0
============================
forall y0 : A, B (fun x1 : A => P x1) y0 -> P y0
subgoal 2 is:
B mu x
のあとどうすればいいでしょうか？上記のsubgoalの中の
(fun x1 : A => P x1)をPに変える命令とかあるんでしょうか？
0116追加
垢版 |
2015/03/19(木) 15:03:19.56ID:g9YALw9l
ちなみに、
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
までが上記の結果です。
0117１３２人目の素数さん
垢版 |
2015/03/23(月) 21:55:09.34ID:hFhIEEUk
>>95
>数学の体系は、公理系によって成り立っている。すなわち、
>当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、
>さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。
>そのように数学は、間違いのない証明によって次々と築き上げるものである。

ゲーデルの不完全性定理によれば
あんたの言ってる事は数学の本性の上っ面でしかない
0121１３２人目の素数さん
垢版 |
2015/04/17(金) 21:21:52.45ID:oyQOgKjs
>>116
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
intro y0.
apply (b y0).
apply a.
Qed.
0123１３２人目の素数さん
垢版 |
2015/04/18(土) 09:18:54.32ID:Q1uVLxMU
直観主義では証明できないので
Require Import Classical.
Variable (p q r:Prop).
Theorem T:((p /\ q) -> r) -> ((p -> r)\/(q -> r)).
Proof.
apply NNPP.
intuition.
Qed.

もっと手を抜くなら
Proof.
tauto.
Qed.
0124１３２人目の素数さん
垢版 |
2015/04/18(土) 10:22:46.84ID:Q1uVLxMU
p, q に関する排中律だけ仮定して

Variable (p q r:Prop).
Hypotheses (EM_p: p\/~p) (EM_q: q\/~q).
Theorem T:((p /\ q) -> r) -> ((p -> r)\/(q -> r)).
Proof.
intro H.
elim EM_p.
intro H0.
elim EM_q.
intro H1.
apply or_introl.
intro.
apply H.
apply conj.
exact H0.
exact H1.
intro.
apply or_intror.
intro.
contradiction.
intro.
apply or_introl.
contradiction.
Qed.
0125１３２人目の素数さん
垢版 |
2015/04/18(土) 11:34:32.18ID:Q1uVLxMU
pに関する排中律だけで

Variable (p q r:Prop).
Hypothesis EM_p: p\/~p.
Theorem T:((p /\ q) -> r) -> ((p -> r)\/(q -> r)).
Proof.
intro H.
elim EM_p.
intro H0.
apply or_intror.
intro H1.
apply H.
apply conj.
exact H0.
exact H1.
intro H2.
apply or_introl.
intro H3.
absurd p.
exact H2.
exact H3.
Qed.
0126115
垢版 |
2015/04/18(土) 16:08:27.46ID:Ch74qrhJ
>>121
レス大感謝です。しかし、
apply (b y0).
のところで、
Error: Impossible to unify "B P y0 -> P y0" with
"B (fun x0 : A => P x0) y0 -> P y0".
と叱られました。Coqのバージョンが
Welcome to Coq 8.3pl3
で古いのでしょうか。
0127122
垢版 |
2015/04/18(土) 18:57:48.32ID:CUF6Decr
>>123-125
ありがとうございます。
知らなったタクティクがいっぱいありますね。
0128１３２人目の素数さん
垢版 |
2015/04/19(日) 20:01:47.33ID:wQv7TFhy
>>126
coq8.4からη変換が入ったみたいね
多分これでη変換無しで行けると思う

Variable A:Type.
Variable B:(A -> Type) -> A -> Type.
Definition mu := fun (x:A) => forall P:(A -> Type), (forall (y:A), B P y -> P y) -> P x.
Hypothesis m : forall (P Q:A -> Type), (forall (x:A), P x -> Q x) -> (forall (x:A), B P x -> B Q x).

Theorem r1:forall (x:A), B mu x -> mu x.
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.

intros y0 c.
apply b.
apply (m (fun x : A => P x) P).
trivial.
exact c.
exact a.
Qed.
0129115
垢版 |
2015/04/21(火) 16:23:18.95ID:X1phHP6G
>>128
レス大感謝です。さて、また私にとって難題です。エラーが出る最小限の
手順を用意しましたので、偉い方、どうかお付き合いください。
第1の例
Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).

Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).

Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b.
Proof.
intros a b Hab.
assert (Hta:(a = b) /\ (b = a)).
apply Ee.
unfold Eqt.
assumption.(*ここでエラーが出ます*)
Qed.

これは、Display implicit argumentsとDeactivate notations display
をすることによって、Implicitな変数が原因であることがわかりました。
0130129
垢版 |
2015/04/21(火) 16:25:47.49ID:X1phHP6G
そこで、次のように証明手順を変えてみると、なんと、最期のassumptionで
Proof completed.が表示されるのに、Qedの後エラーとなるのです。
第2の例
Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).

Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).

Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b.
Proof.
intros a b Hab.
assert (Hta:(a = b) /\ (b = a)).
apply Ee in Hab.
assumption.
elim Hta.
intros H H0.
assumption.
Qed.

どうかお救いください。トホホ
0131１３２人目の素数さん
垢版 |
2015/04/24(金) 23:44:49.27ID:RQUiSeMS
@eq Set a b と @eq Type a b は違う型なのが原因な気がする。
130のようなQedでエラーになるのは結構あって、証明モードの途中ではあんまり頑張って型検査しないから、
こういう微妙な型の差しかないときはしかたないかな。
0132129
垢版 |
2015/04/29(水) 09:13:55.74ID:Z8S8LZWA
レス大感謝です。結局は反則をすることによって解決しました。つまり、
証明法を探すのではなく、>>129の
＞Definition Eqt (A B:Type): Prop := (A = B) \/ (B = A).
の部分を
Definition Eqt (T:Type) (A B:T) : Prop := (eq (A := T) A B) \/ (eq (A := T) B A).
Implicit Arguments Eqt [T].
と変えました。これで、>>129の証明の仕方でもエラーは出なくなりました。
ちなみに最期まで証明すると、
Axiom Ee : forall (a b:Set), Eqt a b -> ((a = b) /\ (b = a)).

Theorem Eab : forall (a b:Set), ((a = b) \/ (b = a)) -> a = b.
Proof.
intros a b Hab.
assert (Hta:(a = b) /\ (b = a)).
apply Ee.
unfold Eqt.
assumption. (*ここでエラーが出ずに先へ進めます*)
elim Hta; intros H1 H2.
assumption.
Qed.
0133１３２人目の素数さん
垢版 |
2015/04/29(水) 21:07:39.24ID:DcI2ISH9
Coqで作られたCコンパイラがあるそうですが、
詳しいことがわかるURLないでしょうか。
■ このスレッドは過去ログ倉庫に格納されています
ニューススポーツなんでも実況