X
トップページ⇒数学
274コメント91KB
【Coq】コンピューターで証明しよう【コック】©2ch.net
■ このスレッドは過去ログ倉庫に格納されています
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ないでしょうか。
0135133
垢版 |
2015/04/30(木) 11:12:49.99ID:YN5jSrOT
ありがとうございます。
読んでみます。
0139１３２人目の素数さん
垢版 |
2015/05/29(金) 21:19:13.70ID:sppsbb3D
Coqだと停止しないコードは書けないそうですが、
停止するコードは必ずCoqでも等価なコードがかけるのかどうか気になります。
書けるんでしょうか？
0140１３２人目の素数さん
垢版 |
2015/06/01(月) 20:03:21.42ID:vP0/D1Ed
停止するかどうかわかるということは停止までのステップ数も見積もれるんでしょうか。
大まかでいいので。
0141１３２人目の素数さん
垢版 |
2015/06/17(水) 02:15:51.60ID:w70GpJG/
Coqそのものの話じゃなくてすいませんが、software foundationsと言うCoqの解説書↓
http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

があって、ここのdownloadから拾ってきたものでPDF作る（make, make pdfする）と章順が逆になって、最初にPostscriptが
最後がPrefaceとSymbolになったものができてしまいます。

正しくmakeできた方いたら、やり方教えて下さい。
0143141
垢版 |
2015/06/21(日) 09:25:51.67ID:szLD4AMj
make all.pdfした時に実行されるcoqdepの出力が逆順になっているので、
これをシェルスクリプトで逆順にしたら、それらしい順番のPDFになりました。
書き忘れましたが、使ってた環境はcoq 8.4pl6です。
お騒がせしました
0144１３２人目の素数さん
垢版 |
2015/06/23(火) 19:05:42.67ID:y39xeCDy
>>142
返信遅れてすいません。
読んでもよく理解できないTT

たとえば２つのプログラムが与えられて、
どちらが後に停止するか、みたいなことはできるんでしょうか。
アッカーマン関数のような巨大な関数との比較がしたいのですが。
0146１３２人目の素数さん
垢版 |
2015/11/02(月) 15:40:58.39ID:voHQlbVG
数学セミナーvol.54 no.11 649
特集　コンピュータにできる数学・できない数学
　Coq:型理論から来た証明支援系, Jacques Garrigue
0147１３２人目の素数さん
垢版 |
2016/05/25(水) 19:39:54.39ID:EB6pp118
質問よろしいでしょうか。
「x>1ならば、そのべき乗は、いつか特定の数を追い抜く」という命題が証明できません。
Require Import Omega.

Theorem multi_inf_gt3:
forall (x : nat), x>1 -> exists m : nat, x^m > 1000.
proof.
intros.
exists 1000.
induction x.
omega.

assert (x>1 -> x^1000<S x^1000).
intro.
apply (Nat.pow_lt_mono_l_iff x (S x) 1000).
auto.
auto.

assert ((x>1->x^1000>1000)->(x>1->x^1000<S x^1000)->(x>1->S x^1000>1000)).
omega.

apply H1 in H0.
apply H0.
apply IHx.
ここで、仮定は「S x > 1」、ゴールは「x > 1」となって、証明できません。
お知恵を貸していただけないでしょうか……
0148１３２人目の素数さん
垢版 |
2016/05/25(水) 20:46:14.27ID:EofZeTbn
まずはこれを解いてみるとか。

Require Import Omega.

Theorem t:
exists m : nat, 2^m > 1000.
0149１３２人目の素数さん
垢版 |
2016/05/25(水) 20:55:32.32ID:EofZeTbn
俺の環境じゃ以下のもOmega解いてくれなかったわ。なぜ？

Theorem t:
2^10 > 1000.
0150１３２人目の素数さん
垢版 |
2016/05/25(水) 23:04:16.75ID:EB6pp118
僕のCoqバージョンはversion 8.5pl1 (April 2016)ですが、
僕もomega単独では解けませんでした。

Theorem t1:
2^10 > 1000.
(* proof. *)
simpl.
omega.
Qed.

Theorem t2:
exists m : nat, 2^m > 1000.
(* proof. *)
exists 10.
simpl.
omega.
Qed.
■ このスレッドは過去ログ倉庫に格納されています
ニューススポーツなんでも実況