【Coq】コンピューターで証明しよう【コック】©2ch.net
■ このスレッドは過去ログ倉庫に格納されています
Coqというプログラムを使えば、計算機上で数学的な証明を厳密に行うことができます。 http://www.iij-ii.co.jp/lab/techdoc/coqt/ http://ja.wikipedia.org/wiki/Coq 使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。 さあ、試してみよう! Coqだと停止しないコードは書けないそうですが、 停止するコードは必ずCoqでも等価なコードがかけるのかどうか気になります。 書けるんでしょうか? 停止するかどうかわかるということは停止までのステップ数も見積もれるんでしょうか。 大まかでいいので。 Coqそのものの話じゃなくてすいませんが、software foundationsと言うCoqの解説書↓ http://www.cis.upenn.edu/ ~bcpierce/sf/current/index.html があって、ここのdownloadから拾ってきたものでPDF作る(make, make pdfする)と章順が逆になって、最初にPostscriptが 最後がPrefaceとSymbolになったものができてしまいます。 正しくmakeできた方いたら、やり方教えて下さい。 >>140 このライブラリを使えばいいんじゃないかな、 https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html nステップ以下で停止するって述語が Hypothesis P_dec : forall n, {P n}+{~(P n)}. を満たしていれば、停止するステップ数を構成してくれるよ。 make all.pdfした時に実行されるcoqdepの出力が逆順になっているので、 これをシェルスクリプトで逆順にしたら、それらしい順番のPDFになりました。 書き忘れましたが、使ってた環境はcoq 8.4pl6です。 お騒がせしました >>142 返信遅れてすいません。 読んでもよく理解できないTT たとえば2つのプログラムが与えられて、 どちらが後に停止するか、みたいなことはできるんでしょうか。 アッカーマン関数のような巨大な関数との比較がしたいのですが。 数学セミナーvol.54 no.11 649 特集 コンピュータにできる数学・できない数学 Coq:型理論から来た証明支援系, Jacques Garrigue 質問よろしいでしょうか。 「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」となって、証明できません。 お知恵を貸していただけないでしょうか…… まずはこれを解いてみるとか。 Require Import Omega. Theorem t: exists m : nat, 2^m > 1000. 俺の環境じゃ以下のもOmega解いてくれなかったわ。なぜ? Theorem t: 2^10 > 1000. 僕の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. simplとやらがカギなのか? 元の問題にもsimpl使えない? omegaは基本的に掛け算には無力 プレスバーガー算術を対象としているから、らしい simplは単に定義に従って簡約してくれる よって>>149 には適用できるが、>>148 はmatchできなくて無理 できました! 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 初心者は必ず騙されるが 証明論とは命題の証明方法の理論ではない ちなみに命題の証明方法は別に難しくない ただ証明がない場合、止まらないので 「アルゴリズム」とは言えないが ■ このスレッドは過去ログ倉庫に格納されています
read.cgi ver 07.5.5 2024/06/08 Walang Kapalit ★ | Donguri System Team 5ちゃんねる