【Coq】コンピューターで証明しよう【コック】©2ch.net
■ このスレッドは過去ログ倉庫に格納されています
Coqというプログラムを使えば、計算機上で数学的な証明を厳密に行うことができます。
http://www.iij-ii.co.jp/lab/techdoc/coqt/
http://ja.wikipedia.org/wiki/Coq
使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。
さあ、試してみよう! できました!
2^10=1024 > 1000を使うのがポイントだったみたいです。
Require Import Omega.
Theorem multi_inf_gt4:
forall (x : nat), x>1 -> exists m : nat, x^m > 1000.
(* proof. *)
intro.
intro.
destruct x.
omega.
exists 10.
assert (S x>1 -> 2^10 <= S x^10).
intro.
apply (Nat.pow_le_mono_l_iff 2 (S x) 10).
auto.
auto.
change (S x > 1 -> 1024 <= S x ^ 10) in H0.
apply H0 in H.
omega.
Qed.
レスして下さった皆様、ありがとうございます。
次は実数でチャレンジするかも!? 実数でもx>2の場合はできました。
x^10を原始的にxで割っていく方法です。 右辺が10000だったらどーするんだwww
Require Import Rbase.
Require Import Fourier.
Theorem multi_inf_gt6:
forall (x : R), x>2 -> exists m : nat, (Rpow_def.pow x m)>1000.
Proof.
intro.
intro.
exists 10%nat.
simpl.
apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.
apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.
apply Rmult_le_0_lt_compat.
fourier.
fourier.
apply H.
assert (2*/2*125=125).
apply Rinv_r_simpl_r.
discrR.
assert (forall (a b c d:R), a*b*c = a*(b*c)).
intros.
ring.
rewrite H1 in H0.
rewrite <- H0.
apply (Rmult_le_0_lt_compat 2 x (/2*125) (x*(x*(x*(x*(x*(x*1)))))) ).
fourier.
fourier.
apply H.
all: cycle 1.
apply x. assert (2*/2*(/2*125)=/2*125).
apply (Rinv_r_simpl_r 2 (/2*125)).
discrR.
rewrite H1 in H2.
rewrite <- H2.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*125)) (x*(x*(x*(x*(x*1))))) ).
fourier.
fourier.
apply H.
assert (2*/2*(/2*(/2*125))=/2*(/2*125)).
apply (Rinv_r_simpl_r 2 (/2*(/2*125)) ).
discrR.
rewrite H1 in H3.
rewrite <- H3.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*125))) (x*(x*(x*(x*1)))) ).
fourier.
fourier.
apply H.
assert ( 2*/2*(/2*(/2*(/2*125))) = /2*(/2*(/2*125)) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*125))) ).
discrR.
rewrite H1 in H4.
rewrite <- H4.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*125)))) (x*(x*(x*1))) ).
fourier.
fourier.
apply H.
assert ( 2*/2*(/2*(/2*(/2*(/2*125)))) = /2*(/2*(/2*(/2*125))) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*(/2*125)))) ).
discrR.
rewrite H1 in H5.
rewrite <- H5.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*(/2*125))))) (x*(x*1)) ).
fourier.
fourier.
apply H.
assert ( 2*/2*(/2*(/2*(/2*(/2*(/2*125))))) = /2*(/2*(/2*(/2*(/2*125)))) ).
apply (Rinv_r_simpl_r 2 (/2*(/2*(/2*(/2*(/2*125))))) ).
discrR.
rewrite H1 in H6.
rewrite <- H6.
apply (Rmult_le_0_lt_compat 2 x (/2*(/2*(/2*(/2*(/2*(/2*125)))))) (x*1) ).
fourier.
fourier.
apply H. fourier.
apply x.
apply x.
apply x.
apply x.
apply x.
Qed.
1<x<2の場合はどうするんだろう? 1<x<2の場合は、lim[x->∞](1+1/x)^x=eをヒントにできないかな、と思っています。
今日のCoq:
Require Import Rbase.
Require Import Fourier.
Lemma l2:
forall (x y:R), y>1 -> x=1+1/y -> 1<x<2.
Proof.
intros.
rewrite H0.
assert (forall (a b:R), a<b -> 1+a<1+b).
intro.
intro.
intro.
fourier.
apply conj.
assert (1+0=1).
ring.
replace (1<1+1/y) with (1+0<1+1/y).
apply (H1 0 (1/y)).
all: cycle 1.
rewrite H2.
reflexivity.
all: cycle 1.
assert (0<1 -> 0<1/y -> 1/y*0<1/y*1).
intro.
apply (Rfourier_lt 0 1 (1/y)).
auto.
assert (1/y*0 = 0).
ring.
rewrite H4 in H3.
assert (1/y*1 = 1/y).
ring.
rewrite H5 in H3.
ここまでで、仮定が0 <1 -> 0<1/ y -> 0 <1/ y、
サブコールが0 < 1 / yで頓挫。。。 >>159を解いても1<x<2 -> x^m>1000に使えなさそうなので、
>>159はあきらめます。 1<x<2 -> x^m>1000、こんな感じになりました。existの形では出来なかったです。
まず1<x<2 -> x^m>2^10を証明して、それから1<x<2 -> x^m>1000を証明しています。
Require Import Rbase.
Require Import Fourier.
Theorem multi_inf_gt7':
forall (x y:R), 1<x<2 ->
x=1+1/y ->
(Rpow_def.pow x (Z.to_nat (up y)))>2 ->
(Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>2*2*2*2*2*2*2*2*2*2.
Proof.
intros.
rewrite Rdef_pow_add.
(↑を9回)
apply Rmult_le_0_lt_compat.
fourier.
fourier.
(↑を9回)
apply H1.
(↑を10回)
Qed. Theorem multi_inf_gt7:
forall (x y:R), 1<x<2 ->
x=1+1/y ->
(Rpow_def.pow x (Z.to_nat (up y)))>2 ->
(Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>1000.
Proof.
intros.
assert ((Rpow_def.pow x ((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))))>2*2*2*2*2*2*2*2*2*2 ->
(Rpow_def.pow x
((Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+
(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))+(Z.to_nat (up y))))>1000).
intro.
fourier.
apply H2.
apply multi_inf_gt7'.
apply H.
apply H0.
apply H1.
Qed. 仮定に使ってる(1+1/y)^y>2ですが、
これをCoqで証明するのは難しそうなので、
このへんにしておきます。 今考えていることを書きます。
1.都内でCoq大会を開きたい。ゲーム形式でCoqの技能を競う。
2.Coqの数式操作をGUIでできるようにしたい。部分数式ごとに適用できるタクティクを「見える化」したい。
3.Coq Twitter BotやCoq onlineを作りたい。 でもOCamlを勉強する時間がないんだ。
やらないといけないことが他にもあるし。 片山さんまだCoq熱冷めてなかったのか。
まあ頑張ってくれ。 日本語の良いチュートリアルが欲しい。
インタラクティブなやつならなお良し。 >>164
onlineはproofwebやらjscoqやらあるしbotの方が面白そうだな
140字でどの程度のことができるのかわからんが proofwebでcoqを使うと、画面の右下にGentzenのproof treeを
表示してくれるのですが、その機能をローカルに自分のパソコンでも
使えるようにできるのですか?できるのでしたらやり方を教えてもらえないで
しょうか。 >>172
レスありがとうございます。でも今Linuxは無理です。
残念です。 >>173
仮想環境のVirtualBoxを使う手がある。 苗■
405 : 猫は唯の馬鹿 ◆MuKUnGPXAY [age] 投稿日:2011/04/09(土) 15:29:50.46
猫 ★★★数学徒は馬鹿板をしない生活を送り、日頃から真面目に学問に精進すべき。★★★
¥ ★★★数学徒は馬鹿板をしない生活を送り、日頃から真面目に学問に精進すべき。★★★
¥ Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化
https://goo.gl/ji1QUd 将来的にはコンピュータは数学者になれるのでしょうか? >>7
> English speakerに前置きなく「コック」って言ったら誤解を産むよね
日本語話者にも開発者のCoquandの名前を「コカン」って呼んだら誤解生みそう
「Coqはコカンが生みました」
????? 数学の教科書をcoqで翻訳して公開したら著作権違反になりますか? これでMathematicaみたいなことができるの? >>207
それは翻訳じゃなくて詳細な機械証明をつけたことになるからいいんじゃね?
やれるもんならやってごらん(挑発) 1700
学コン・宿題ボイコット実行委員会@gakkon_boycott 9月1日
#拡散希望
#みんなで学コン・宿題をボイコットしよう
雑誌「大学への数学」の誌上で毎月開催されている学力コンテスト(学コン)と宿題は、添削が雑で採点ミスが多く、訂正をお願いしても応じてもらえない悪質なコンテストです。(私も7月号の宿題でその被害に遭いました。)このようなコンテストに参加するのは時間と努力の無駄であり、参加する価値はありません。そこで私は、これ以上の被害者を出さないようにするため、また、出版社に反省と改善を促すために、学コン・宿題のボイコットを呼び掛けることにしました。少しでも多くの方がこの活動にご賛同頂き、このツイートを拡散して頂ければ幸いです。
https://twitter.com/gakkon_boycott/status/1300459618326388737
https://twitter.com/5chan_nel (5ch newer account) >>209
ありがとうございます😊
やってみようと思います。 Coqとかのソフトウェアを理解して使えるようになるには,どんな本を読めばいいですか? 本なら『Coq/SSReflect/MathCompによる定理証明』かな。実際に使って証明したいものを証明した方が良いと思うけど。 >>213
ありがとうございます.
その本は読んだことがあるのですが,何が書いてあるのかよくわかりませんでした.
その本を読むための予備知識はどんな本を読めばいいのでしょうか? Coqで何をしたいのかは分からないけど、数学の証明をしたいのなら命題論理とか述語論理の勉強をしたらいいと思うよ。 プログラムの観点から言うと、「依存型」「カリー=ハワード同型対応」がキーワードになるかな。
あんまり伸びてないけど、ム板にこういうスレがある。
【F*】依存型っていいの?【Coq】
https://mevius.5ch.net/test/read.cgi/tech/1554809503/ F x = If x < 10 then x else F (x - 1)
みたいな関数ってCoqでどう性質を証明しますか?ifの条件で場合分けしたいです
タクティックでcase ( x< 10)としても、
仮説にならないで、場合わけにならずに困っています。 >>218
まさにこれっぽいです。ありがとうございます! Coqで日本語データを処理するプログラム書けますか?
Asciiは扱えるみたいです。 https://www.iij-ii.co.jp/activities/programming-coq/coqt1.html
これの練習問題の2つ目が分からない。
>問1. 任意の命題 A B C に対して、「A ならば B ならば C」ならば「B ならば A ならば C」が成り立つ。
要するにこれはB⇒Aが可能なら、前提条件からA⇒Cだと思ったけど。
どう書くの?全然分からん
Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C):=
fun A B C a b c => ?. >>221
Definition prop4 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C) :=
fun A B C f b a => f a b.
かな。f の型が (A -> B -> C) で、b の型が B で、a の型が A 。
「ならば」(->) は右結合だから、(B -> A -> C) の部分の括弧は外す事ができる。 | \
|Д`) ダレモイナイ・・オドルナラ イマノウチ
|⊂
|
♪ Å
♪ / \ ランタ タン
ヽ(´Д`;)ノ ランタ タン
( へ) ランタ ランタ
く タン
♪ Å
♪ / \ ランタ ランタ
ヽ(;´Д`)ノ ランタ タン
(へ ) ランタ タンタ
> タン | \
|Д`) ダレモイナイ・・オドルナラ イマノウチ
|⊂
|
♪ Å
♪ / \ ランタ タン
ヽ(´Д`;)ノ ランタ タン
( へ) ランタ ランタ
く タン
♪ Å
♪ / \ ランタ ランタ
ヽ(;´Д`)ノ ランタ タン
(へ ) ランタ タンタ
> タン ゲーデルの不完全性定理の証明とか、
選択公理が命題として他の公理とは独立であることの証明とかできるかな?
もっと素朴に、√2が有理数では無いことの証明とか、
eやπが有理数ではないことの証明とか、
複素数係数の代数方程式は複素数の根を必ず持つことの証明とか。。。 このようなソフトウェアに興味があるのですが、使えるようになるには、「証明論」のような本を
勉強しないとだめですよね。 >>231
数学の知識よりも、プログラミングの知識のほうが重要だと思う。
関数型言語についてとか。 >>229
>ゲーデルの不完全性定理の証明
無矛盾(矛盾が証明されない)ならば
無矛盾性が証明されない、と読むから
神秘性や難しさを感じる
矛盾が証明されると矛盾する、という証明から
矛盾の証明が出来る、と読めばただのトリック >>231
初心者は必ず騙されるが
証明論とは命題の証明方法の理論ではない
ちなみに命題の証明方法は別に難しくない
ただ証明がない場合、止まらないので
「アルゴリズム」とは言えないが >>229
> √2が有理数では無いことの証明
Coqと同様の定理証明支援系であるHOL LightのTutorialに
11.1 Irrationality of √2がある
www.cl.cam.ac.uk/~jrh13/hol-light
実際にそこで証明しているのは
∀p,q. p×p=2×q×q ⇒ q=0 だけど >>232
数学とプログラミングが統一される前に時間切れでシンギュラリティが来そう。 証明が存在する命題は、有限回の操作によって必ず証明にたどり着く方法はある。
ただし、その有限回なる回数が一体どのぐらいの有限なのかだ。宇宙が終わるまで
かけても終わらない程の大きな回数であっても有限だから。 ある命題の成立に対して正しい証明が得られたならば、
その証明が正しいことを確認する作業は、必ず証明の
記述の長さの多項式オーダーの手間で可能なのだろうか? (Coqのような)証明系は正しい証明を記述したならば、それが正しいことを
必ず有限の時間で検証を終えて停止するのだろうか?
その有限の時間だといっても途方も無く長くなったりしないのだろうか?
検証を行う前に、証明の記述に応じてそれに対する検証時間の上界が
事前に得られるものだろうか?
それともそのような上界は一般にはなくて、ただただ結果が出るまで
ずーっと待って運良く生きているうちに終わることを期せねばならないのだろうか?
C言語とかAlgolのような普通のプログラミング言語は、
コンパイルすべきプログラムの長さNに対するコンパイル完了までの時間は
O(N log N)程度になってる。もしもコンパイルの時間がたとえばO(N^2)
かかるような言語とかコンパイラであると、プログラムの記述が大規模になれば
実用性が低くて使い物にならない感じになる。 >>240
証明になっているか否かのチェックは有限時間で可能
証明になってないギャップについて
ギャップが埋められるかどうかは
命題が証明できるかどうかと同じなので
有限時間では判定できない 「証明」の長さがNであるときに、検証にかかる計算量がNについてあまり急増化
しないのであれば、検証システムは使い物になるが、Nについてたとえば多項式
オーダーではなかったならば、少しばかり長い「証明」を検証しようとすれば
現実的には「いつまでたっても終わらないなぁsigh、修論が落ちるな」、
ということになりそうだけれども、そのあたりはどうなっているのでしょうか? 検証系が進歩した未来において、
著者は自分の証明を検証系にかけて、
検証系に与えたソースコードも併せて提出する。
論文の査読者はそのソースコードが正しく論文の定理や命題を表していることを
(ああたいへんだ)チェックして(そこが間違ってたらどうする?)、
検証系にかけて、正しく証明されることを確認したら、アクセプトする。
そうなったらとても面倒。論文のLaTeXのソースを提出するのとは次元が違う。 ABC予想の証明の検証に時間がかかっていたようだけど、
Coqで検証すればよかったんじゃないの?できないの? 人間の書いた人間に理解できるように書かれた証明を、
いろいろな前提知識の無い無垢のソフトに全く隙のない形で
完璧に記号だけを使って記述し直すというのは、とても大変な
作業になるだろう。暗黙知、専門家の常識、そういうものを総動員して
それらも含めて検証にかけなければ、論理が飛んでいることになるから
だろう。 ABC予想の証明に否定的な数学者もいるようですから、
白黒はっきりつけるためにはした方が良さそうですね
おそろしく時間とお金(人件費)が掛かりそうですが… 今まで正しいと思われていた定理がCoqで検証をしたら証明が間違っていて実は成立していなかった
という場合はあり得るのだろうか? 定理をみな洗濯して候。選択公理を密輸入してたりとか。 基本的な質問で申し訳ありませんが、任意の数学の定理の証明は
その証明が正しいならばコンピューターが理解できる形の形式的な証明に書き直せますよね? >>249
非構成的な証明とかは、形式的な証明に落とし込めるのかなあ? 数学によってはインフォーマルな証明ってのがあるかも 数学を外から眺めているメタ数学、そのメタ数学を外から眺めているメタメタ数学、
そのメタメタ数学を外から眺めているメタメタメタ数学、とどこまでいっても
その外側から眺めている数学があるのだとしたら。この宇宙も、メタ宇宙の中で
眺められ観察され実験されている存在なのじゃないかと思えてくる。
ある日、これじゃダメだな、やり直すかという声が聞こえてきて。。。 ■ このスレッドは過去ログ倉庫に格納されています