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

2015/01/23(金) 01:41:03.17

Coqというプログラムを使えば、計算機上で数学的な証明を厳密に行うことができます。

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

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

**１３２人目の素数さん** · 2015/02/11(水) 20:46:57.00

>>101
それは前から分かっていること

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/02/13(金) 02:36:25.72

同値変換だけで命題論理式を最も単純な節形式にするって未解決だよな？

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/02/13(金) 13:45:35.78

クワイン・マクラスキー法
http://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%AF%E3%82%A4%E3%83%B3%E3%83%BB%E3%83%9E%E3%82%AF%E3%83%A9%E3%82%B9%E3%82%AD%E3%83%BC%E6%B3%95

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/02/13(金) 17:47:55.74

NP困難なんて気合いと悪運で突破する！

**１３２人目の素数さん** · 2015/02/13(金) 20:56:57.57

せめて近似で突破して

**１３２人目の素数さん** · 2015/02/16(月) 06:52:55.96

私、O'Camlなどでのプログラミング経験はあるが数学の力に自信がないもので、数学書を一人で読み進める時にきちんと証明出来ている確信が欲しくて久しぶりにCoqを触り始めました。
証明のコードを生成してみるのもまた愉し。

**１３２人目の素数さん** · 2015/02/16(月) 11:44:48.02

>>86もう無理でしょうか。しくしく。

**１３２人目の素数さん** · 2015/02/16(月) 19:45:39.73

Coqってグッドスタイン数列の収束は証明できるの？

**１３２人目の素数さん** · 2015/03/17(火) 05:27:20.77

検証はイメージできるけど証明か

**１３２人目の素数さん** · 2015/03/17(火) 11:09:06.79

検証と証明ってどう違うの
一例の場合か全ての場合かってこと？

**１３２人目の素数さん** · 2015/03/17(火) 12:42:17.91

具体的に人間が与えた証明が正しい推論になっているか確かめるのが検証。
証明システムなら人工知能が結論までの道筋を自ら見つけるということになるはず。

**１３２人目の素数さん** · 2015/03/17(火) 21:53:44.21

Coqって順序数扱えんの？

**１３２人目の素数さん** · 2015/03/19(木) 15:02:35.75

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に変える命令とかあるんでしょうか？

追加 · 2015/03/19(木) 15:03:19.56

ちなみに、
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
までが上記の結果です。

**１３２人目の素数さん** · 2015/03/23(月) 21:55:09.34

>>95
>数学の体系は、公理系によって成り立っている。すなわち、
>当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、
>さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。
>そのように数学は、間違いのない証明によって次々と築き上げるものである。

ゲーデルの不完全性定理によれば
あんたの言ってる事は数学の本性の上っ面でしかない

**１３２人目の素数さん** · 2015/04/13(月) 14:47:42.65

ここは死んでしまったのでしょうか。しくしく。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/04/13(月) 16:42:48.12

すまね。仕事で忙しい、疲れてるときは数学ができない。

**１３２人目の素数さん** · 2015/04/13(月) 19:17:53.26

景気いいの？
浦山

**１３２人目の素数さん** · 2015/04/17(金) 21:21:52.45

>>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.

**１３２人目の素数さん** · 2015/04/17(金) 22:20:53.23

((p∧q)→r)→((p→r)∨(q→r))
は証明できますか

**１３２人目の素数さん** · 2015/04/18(土) 09:18:54.32

直観主義では証明できないので
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.

**１３２人目の素数さん** · 2015/04/18(土) 10:22:46.84

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.

**１３２人目の素数さん** · 2015/04/18(土) 11:34:32.18

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.

**115** · 2015/04/18(土) 16:08:27.46

>>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
で古いのでしょうか。

**122** · 2015/04/18(土) 18:57:48.32

>>123-125
ありがとうございます。
知らなったタクティクがいっぱいありますね。

**１３２人目の素数さん** · 2015/04/19(日) 20:01:47.33

>>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.

**115** · 2015/04/21(火) 16:23:18.95

>>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な変数が原因であることがわかりました。

**129** · 2015/04/21(火) 16:25:47.49

そこで、次のように証明手順を変えてみると、なんと、最期の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.

どうかお救いください。トホホ

**１３２人目の素数さん** · 2015/04/24(金) 23:44:49.27

@eq Set a b と @eq Type a b は違う型なのが原因な気がする。
130のようなQedでエラーになるのは結構あって、証明モードの途中ではあんまり頑張って型検査しないから、
こういう微妙な型の差しかないときはしかたないかな。

**129** · 2015/04/29(水) 09:13:55.74

レス大感謝です。結局は反則をすることによって解決しました。つまり、
証明法を探すのではなく、>>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.

**１３２人目の素数さん** · 2015/04/29(水) 21:07:39.24

Coqで作られたCコンパイラがあるそうですが、
詳しいことがわかるURLないでしょうか。

**１３２人目の素数さん** · 2015/04/29(水) 21:13:19.95

>>133
http://compcert.inria.fr/compcert-C.html

**133** · 2015/04/30(木) 11:12:49.99

ありがとうございます。
読んでみます。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/05/05(火) 22:36:38.53

>>134
こりゃすげーや

**１３２人目の素数さん** · 2015/05/06(水) 11:27:30.01

なにがどうすごいのか3行でplz

**１３２人目の素数さん** · 2015/05/17(日) 09:28:41.49

Cock!

**１３２人目の素数さん** · 2015/05/29(金) 21:19:13.70

Coqだと停止しないコードは書けないそうですが、
停止するコードは必ずCoqでも等価なコードがかけるのかどうか気になります。
書けるんでしょうか？

**１３２人目の素数さん** · 2015/06/01(月) 20:03:21.42

停止するかどうかわかるということは停止までのステップ数も見積もれるんでしょうか。
大まかでいいので。

**１３２人目の素数さん** · 2015/06/17(水) 02:15:51.60

Coqそのものの話じゃなくてすいませんが、software foundationsと言うCoqの解説書↓
http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

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

正しくmakeできた方いたら、やり方教えて下さい。

**１３２人目の素数さん** · 2015/06/19(金) 00:07:06.67

>>140
このライブラリを使えばいいんじゃないかな、
https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html

nステップ以下で停止するって述語が
Hypothesis P_dec : forall n, {P n}+{~(P n)}.
を満たしていれば、停止するステップ数を構成してくれるよ。

**141** · 2015/06/21(日) 09:25:51.67

make all.pdfした時に実行されるcoqdepの出力が逆順になっているので、
これをシェルスクリプトで逆順にしたら、それらしい順番のPDFになりました。
書き忘れましたが、使ってた環境はcoq 8.4pl6です。
お騒がせしました

**１３２人目の素数さん** · 2015/06/23(火) 19:05:42.67

>>142
返信遅れてすいません。
読んでもよく理解できないTT

たとえば２つのプログラムが与えられて、
どちらが後に停止するか、みたいなことはできるんでしょうか。
アッカーマン関数のような巨大な関数との比較がしたいのですが。

**１３２人目の素数さん** · 2015/10/14(水) 23:33:20.11

数蝉

**１３２人目の素数さん** · 2015/11/02(月) 15:40:58.39

数学セミナーvol.54 no.11 649
特集　コンピュータにできる数学・できない数学
　Coq:型理論から来た証明支援系, Jacques Garrigue

**１３２人目の素数さん** · 2016/05/25(水) 19:39:54.39

質問よろしいでしょうか。
「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」となって、証明できません。
お知恵を貸していただけないでしょうか……

**１３２人目の素数さん** · 2016/05/25(水) 20:46:14.27

まずはこれを解いてみるとか。

Require Import Omega.

Theorem t:
exists m : nat, 2^m > 1000.

**１３２人目の素数さん** · 2016/05/25(水) 20:55:32.32

俺の環境じゃ以下のもOmega解いてくれなかったわ。なぜ？

Theorem t:
2^10 > 1000.

**１３２人目の素数さん** · 2016/05/25(水) 23:04:16.75

僕の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.

**１３２人目の素数さん** · 2016/05/25(水) 23:09:57.26

simplとやらがカギなのか？
元の問題にもsimpl使えない？

**１３２人目の素数さん** · 2016/05/25(水) 23:39:51.15

omegaは基本的に掛け算には無力
プレスバーガー算術を対象としているから、らしい

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

**１３２人目の素数さん** · 2016/05/26(木) 00:17:18.47

できました！
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.

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

**１３２人目の素数さん** · 2016/05/26(木) 00:27:48.31

destruct x.もいらないっすね。

**１３２人目の素数さん** · 2016/05/27(金) 03:19:24.12

実数でも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.

**１３２人目の素数さん** · 2016/05/27(金) 03:25:03.30

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.

**１３２人目の素数さん** · 2016/05/27(金) 03:29:56.38

fourier.
apply x.
apply x.
apply x.
apply x.
apply x.
Qed.

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

**１３２人目の素数さん** · 2016/05/27(金) 20:02:06.84

なんかカオスだなｗ
俺は力になれないが頑張れｗ

**１３２人目の素数さん** · 2016/05/30(月) 01:07:49.80

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で頓挫。。。

**１３２人目の素数さん** · 2016/06/01(水) 00:50:01.33

>>159を解いても1<x<2 -> x^m>1000に使えなさそうなので、
>>159はあきらめます。

**１３２人目の素数さん** · 2016/06/01(水) 20:28:33.76

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.

**１３２人目の素数さん** · 2016/06/01(水) 20:31:57.00

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.

**１３２人目の素数さん** · 2016/06/01(水) 20:37:28.80

仮定に使ってる(1+1/y)^y>2ですが、
これをCoqで証明するのは難しそうなので、
このへんにしておきます。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2016/07/04(月) 17:27:13.86

今考えていることを書きます。

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

**片山博文MZ** ◆T6xkBnTXz7B0 · 2016/07/04(月) 17:34:29.59

でもOCamlを勉強する時間がないんだ。
やらないといけないことが他にもあるし。

**１３２人目の素数さん** · 2016/07/04(月) 19:40:12.12

片山さんまだＣｏｑ熱冷めてなかったのか。
まあ頑張ってくれ。

**１３２人目の素数さん** · 2016/07/04(月) 20:23:53.31

日本語の良いチュートリアルが欲しい。
インタラクティブなやつならなお良し。

**１３２人目の素数さん** · 2016/07/04(月) 21:14:49.99

>>164
onlineはproofwebやらjscoqやらあるしbotの方が面白そうだな
140字でどの程度のことができるのかわからんが

**１３２人目の素数さん** · 2016/07/06(水) 11:09:19.26

夏休みの友
http://gathery.recruit-lifestyle.co.jp/article/1146775541637910801

**１３２人目の素数さん** · 2016/07/07(木) 23:26:31.83

数学苦手な俺おわた

**１３２人目の素数さん** · 2016/07/08(金) 09:21:21.88

proofwebでcoqを使うと、画面の右下にGentzenのproof treeを
表示してくれるのですが、その機能をローカルに自分のパソコンでも
使えるようにできるのですか？できるのでしたらやり方を教えてもらえないで
しょうか。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2016/07/08(金) 23:48:26.99

>>171
http://proofweb.cs.ru.nl/install.php

**171** · 2016/07/09(土) 13:47:50.56

>>172
レスありがとうございます。でも今Linuxは無理です。
残念です。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2016/07/10(日) 23:00:19.52

>>173
仮想環境のVirtualBoxを使う手がある。

**１３２人目の素数さん** · 2016/10/05(水) 09:24:20.79

あ

**１３２人目の素数さん** · 2017/06/18(日) 16:49:48.59

苗■

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

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:35:53.09

★★★数学徒は馬鹿板をしない生活を送り、日頃から真面目に学問に精進すべき。★★★

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:51:22.79

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:51:43.36

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:52:04.31

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:52:25.55

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:52:46.45

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:53:06.29

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:53:32.46

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:53:52.62

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:54:12.00

￥

￥ ◆2VB8wsVUoo · 2017/06/18(日) 17:54:31.69

￥

**１３２人目の素数さん** · 2017/06/19(月) 03:33:30.63

ssreflect使わないんか？

**１３２人目の素数さん** · 2017/06/19(月) 04:25:28.67

通常のCoqより難しそうですよね。

￥ ◆2VB8wsVUoo · 2017/06/19(月) 05:24:06.21

★★★数学徒は馬鹿板をしない生活を送り、日頃から真面目に学問に精進すべき。★★★

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:24:06.41

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:24:23.72

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:24:43.20

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:25:01.34

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:25:18.52

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:25:36.12

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:25:54.24

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:26:18.53

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:26:35.36

￥

￥ ◆2VB8wsVUoo · 2017/06/19(月) 07:26:54.38

￥

**１３２人目の素数さん** · 2018/06/21(木) 03:26:55.51

Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化
https://goo.gl/ji1QUd

**１３２人目の素数さん** · 2018/08/14(火) 12:06:55.58

将来的にはコンピュータは数学者になれるのでしょうか？

**１３２人目の素数さん** · 2018/10/17(水) 09:46:19.60

数学者の定義しだい