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

1片山博文MZ ◆T6xkBnTXz7B0 転載ダメ©2ch.net2015/01/23(金) 01:41:03.17ID:kQ1pk3tS
Coqというプログラムを使えば、計算機上で数学的な証明を厳密に行うことができます。

http://www.iij-ii.co.jp/lab/techdoc/coqt/
http://ja.wikipedia.org/wiki/Coq

使いこなすには、大学レベルの数学と論理学とプログラミングと英語の知識が必要。
さあ、試してみよう!

152132人目の素数さん2016/05/25(水) 23:39:51.15ID:fzY8lffh
omegaは基本的に掛け算には無力
プレスバーガー算術を対象としているから、らしい

simplは単に定義に従って簡約してくれる
よって>>149には適用できるが、>>148はmatchできなくて無理

153132人目の素数さん2016/05/26(木) 00:17:18.47ID:vUOIQwNh
できました!
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.

レスして下さった皆様、ありがとうございます。
次は実数でチャレンジするかも!?

154132人目の素数さん2016/05/26(木) 00:27:48.31ID:vUOIQwNh
destruct x.もいらないっすね。

155132人目の素数さん2016/05/27(金) 03:19:24.12ID:ItPB2mak
実数でも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.

156132人目の素数さん2016/05/27(金) 03:25:03.30ID:ItPB2mak
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.

157132人目の素数さん2016/05/27(金) 03:29:56.38ID:ItPB2mak
fourier.
apply x.
apply x.
apply x.
apply x.
apply x.
Qed.

1<x<2の場合はどうするんだろう?

158132人目の素数さん2016/05/27(金) 20:02:06.84ID:Se9f3cOm
なんかカオスだなw
俺は力になれないが頑張れw

159132人目の素数さん2016/05/30(月) 01:07:49.80ID:nh+30MzG
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で頓挫。。。

160132人目の素数さん2016/06/01(水) 00:50:01.33ID:Ih6s2JtZ
>>159を解いても1<x<2 -> x^m>1000に使えなさそうなので、
>>159はあきらめます。

161132人目の素数さん2016/06/01(水) 20:28:33.76ID:Ih6s2JtZ
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.

162132人目の素数さん2016/06/01(水) 20:31:57.00ID:Ih6s2JtZ
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.

163132人目の素数さん2016/06/01(水) 20:37:28.80ID:Ih6s2JtZ
仮定に使ってる(1+1/y)^y>2ですが、
これをCoqで証明するのは難しそうなので、
このへんにしておきます。

164片山博文MZ ◆T6xkBnTXz7B0 2016/07/04(月) 17:27:13.86ID:I+l74NfK
今考えていることを書きます。

1.都内でCoq大会を開きたい。ゲーム形式でCoqの技能を競う。
2.Coqの数式操作をGUIでできるようにしたい。部分数式ごとに適用できるタクティクを「見える化」したい。
3.Coq Twitter BotやCoq onlineを作りたい。

165片山博文MZ ◆T6xkBnTXz7B0 2016/07/04(月) 17:34:29.59ID:I+l74NfK
でもOCamlを勉強する時間がないんだ。
やらないといけないことが他にもあるし。

166132人目の素数さん2016/07/04(月) 19:40:12.12ID:lwP0CPv1
片山さんまだCoq熱冷めてなかったのか。
まあ頑張ってくれ。

167132人目の素数さん2016/07/04(月) 20:23:53.31ID:lwP0CPv1
日本語の良いチュートリアルが欲しい。
インタラクティブなやつならなお良し。

168132人目の素数さん2016/07/04(月) 21:14:49.99ID:b2jsrh3I
>>164
onlineはproofwebやらjscoqやらあるしbotの方が面白そうだな
140字でどの程度のことができるのかわからんが

169132人目の素数さん2016/07/06(水) 11:09:19.26ID:udLxg5Zs

170132人目の素数さん2016/07/07(木) 23:26:31.83ID:18Figzy7
数学苦手な俺おわた

171132人目の素数さん2016/07/08(金) 09:21:21.88ID:LlF6GjmQ
proofwebでcoqを使うと、画面の右下にGentzenのproof treeを
表示してくれるのですが、その機能をローカルに自分のパソコンでも
使えるようにできるのですか?できるのでしたらやり方を教えてもらえないで
しょうか。

172片山博文MZ ◆T6xkBnTXz7B0 2016/07/08(金) 23:48:26.99ID:V/uvjwWo

1731712016/07/09(土) 13:47:50.56ID:n5Zs2sWR
>>172
レスありがとうございます。でも今Linuxは無理です。
残念です。

174片山博文MZ ◆T6xkBnTXz7B0 2016/07/10(日) 23:00:19.52ID:ls3rHzpz
>>173
仮想環境のVirtualBoxを使う手がある。

175132人目の素数さん2016/10/05(水) 09:24:20.79ID:gUCeq6IM

176132人目の素数さん2017/06/18(日) 16:49:48.59ID:v2schHZM
苗■

405 : 猫は唯の馬鹿 ◆MuKUnGPXAY [age] 投稿日:2011/04/09(土) 15:29:50.46

177◆2VB8wsVUoo 2017/06/18(日) 17:35:53.09ID:ze+BLRMV
★★★数学徒は馬鹿板をしない生活を送り、日頃から真面目に学問に精進すべき。★★★


178◆2VB8wsVUoo 2017/06/18(日) 17:51:22.79ID:ze+BLRMV

179◆2VB8wsVUoo 2017/06/18(日) 17:51:43.36ID:ze+BLRMV

180◆2VB8wsVUoo 2017/06/18(日) 17:52:04.31ID:ze+BLRMV

181◆2VB8wsVUoo 2017/06/18(日) 17:52:25.55ID:ze+BLRMV

182◆2VB8wsVUoo 2017/06/18(日) 17:52:46.45ID:ze+BLRMV

183◆2VB8wsVUoo 2017/06/18(日) 17:53:06.29ID:ze+BLRMV

184◆2VB8wsVUoo 2017/06/18(日) 17:53:32.46ID:ze+BLRMV

185◆2VB8wsVUoo 2017/06/18(日) 17:53:52.62ID:ze+BLRMV

186◆2VB8wsVUoo 2017/06/18(日) 17:54:12.00ID:ze+BLRMV

187◆2VB8wsVUoo 2017/06/18(日) 17:54:31.69ID:ze+BLRMV

188132人目の素数さん2017/06/19(月) 03:33:30.63ID:CqOV8oGi
ssreflect使わないんか?

189132人目の素数さん2017/06/19(月) 04:25:28.67ID:YjcAzZZa
通常のCoqより難しそうですよね。

190◆2VB8wsVUoo 2017/06/19(月) 05:24:06.21ID:pqzlCEdf
★★★数学徒は馬鹿板をしない生活を送り、日頃から真面目に学問に精進すべき。★★★


191◆2VB8wsVUoo 2017/06/19(月) 07:24:06.41ID:pqzlCEdf

192◆2VB8wsVUoo 2017/06/19(月) 07:24:23.72ID:pqzlCEdf

193◆2VB8wsVUoo 2017/06/19(月) 07:24:43.20ID:pqzlCEdf

194◆2VB8wsVUoo 2017/06/19(月) 07:25:01.34ID:pqzlCEdf

195◆2VB8wsVUoo 2017/06/19(月) 07:25:18.52ID:pqzlCEdf

196◆2VB8wsVUoo 2017/06/19(月) 07:25:36.12ID:pqzlCEdf

197◆2VB8wsVUoo 2017/06/19(月) 07:25:54.24ID:pqzlCEdf

198◆2VB8wsVUoo 2017/06/19(月) 07:26:18.53ID:pqzlCEdf

199◆2VB8wsVUoo 2017/06/19(月) 07:26:35.36ID:pqzlCEdf

200◆2VB8wsVUoo 2017/06/19(月) 07:26:54.38ID:pqzlCEdf

201132人目の素数さん2018/06/21(木) 03:26:55.51ID:8q3uDaQP
Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化
https://goo.gl/ji1QUd

202132人目の素数さん2018/08/14(火) 12:06:55.58ID:vXAVUkp6
将来的にはコンピュータは数学者になれるのでしょうか?

新着レスの表示
レスを投稿する