【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

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

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 01:51:30.31

自然数nに対する2n＝n＋nの証明の例。

Require Import Arith.
Theorem t: forall n:nat, 2*n = n+n.
intros.
replace (n+n) with (1*n + 1*n).
replace 2 with (1+1).
apply mult_plus_distr_r.
auto.
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
Qed.

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 01:56:25.68

自然数nに対してn (n＋1)が偶数であることの証明の例。

Require Import Even.
Theorem t:forall n:nat, even (n * (1+n)).
intros.
apply even_mult_aux.
elim n.
left.
apply even_O.
intros.
elim H.
right.
apply even_S.
apply odd_S.
apply H0.
left.
apply H0.
Qed.

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 02:10:51.92

Coqは証明支援システムです。数学論文を英語で書ける程度の素養が必要です。
まずはTutorialを読むことから始めましょう。
natは自然数(natural numbers)の略です。
Coqでは英語や英語の略語がよく使われます。

**１３２人目の素数さん** · 2015/01/23(金) 13:44:42.12

自動的に証明ができるんじゃないだろ
そこんとこ誤解させんなよ

**１３２人目の素数さん** · 2015/01/23(金) 13:50:52.34

　　　　　＿＿＿_
　　　　／⌒　　⌒＼
　　　／　癶　　癶　＼
　／::::::⌒（__人__）⌒::::: ＼　　　あらあらうふふ
　 |　　　　　|r┬-|　　　　　|
　＼　　　 `ー'´ 　　／

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 16:34:52.63

>>5
すみません。

>>6
English speakerに前置きなく「コック」って言ったら誤解を産むよね。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 16:42:51.44

「Require Import Arith.」は、
「Arith」というモジュール(部品)を読み込むコマンドだ。
コマンド「Theorem t: forall n:nat, 2*n = n+n.」について。
「Theorem t:」は、これから「t」という名前の定理を証明するよって意味。
「forall n:nat,」は、「∀n∈Ｎ」という意味。
ここで「∀」は論理学における「任意の…に対して」という意味。
「∈」は集合論の「…に属する」に相当する。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 16:48:37.07

掛け算について現在の定義を調べたいなら、掛け算の略は「mult」だから、「SearchAbout mult.」というコマンドを入力すればいい。
自然数について調べたいなら「SearchAbout nat.」を入力。
足し算なら「SearchAbout plus.」。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 16:57:07.60

Theoremコマンドを入力したら、証明モードに入る。
証明モードでは、証明するための「タクティク」(戦術)を入力できる。
コマンドは大文字で始まるが、タクティクは小文字で始まる。
タクティクの例を挙げると、intros,symmetry,left,right,auto,elim,applyなど、いろんなタクティクがある。
証明の終わりでは「Qed.」コマンドを入力する。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 17:12:06.01

さて、Coqのダウンロードとインストールが終わったら、早速Coqを起動しよう。
黒い画面に「Coq <」と表示されるだろう。
これはCoqのプロンプトであり、入力待ちであることを表している。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/23(金) 17:15:42.51

Coqの終了コマンドは「Quit.」である。「Quit.」と打ち込んでEnterキーを押せば
黒い画面が消えるであろう。

**１３２人目の素数さん** · 2015/01/23(金) 21:55:31.77

suck my coq!

**１３２人目の素数さん** · 2015/01/23(金) 23:54:02.33

まずは1がなんかお題だせよ。

**１３２人目の素数さん** · 2015/01/24(土) 00:15:52.39

Coqは数学、プログラミング両方で高い水準を要求されるからな。
このスレは人集まらないだろう。
数板ではプログラムの素養がネックになるか？

**１３２人目の素数さん** · 2015/01/24(土) 00:29:02.73

証明支援系のプログラムにバグがないことはどうやって
証明するの？

**１３２人目の素数さん** · 2015/01/24(土) 08:29:32.31

meta coqを使いなさい

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/24(土) 09:04:43.49

お題：
x^2 - 2x + 1 ＝ (x - 1)^2の証明。

**１３２人目の素数さん** · 2015/01/24(土) 13:04:41.68

>>15
いやいや、いいスレだ。せいぜい集まろうぜ

**１３２人目の素数さん** · 2015/01/24(土) 17:26:49.57

-を+に変えた版はできた。
-の方はまだできてない。

Require Import Omega.
Require Import Arith.
Theorem t:forall n:nat,n*n+2*n+1=(n+1)*(n+1).
intros.
replace (2*n) with (n+n).
symmetry.
replace ((n+1)*(n+1)) with (n*(n+1)+1*(n+1)).
replace (n*(n+1)) with (n*n+n*1).
omega.
symmetry.
apply mult_plus_distr_l.
symmetry.
apply mult_plus_distr_r.
omega.
Qed.

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/24(土) 20:21:46.13

>>20
もう少しだな。-2x＝+(-2)xを使えば、できるはずだ。

**１３２人目の素数さん** · 2015/01/24(土) 22:01:32.97

　　　　　　　／⌒ヽ⌒ヽ
　　　　　　　　Ｙ
　　　　　　　　　　八　　ヽ
　　　　　（　　 __／/.　ヽ,, ,）
　　　　　丶1　　　八.　 !/
　　　　　　 ζ, 　　八.　 j
　　　　　　i　　　丿､　j
　　　　　　 |　　　八　 |
　　　　　　 | !　　　 i　､　|
　　　　　　 | i し　"　i　　'|
　　　　　　|ﾉ　(　　　i　　 i|
　　　　　 (　'~ヽ　　　!　　∥
　　　　 │　　　　i　　∥
　　　　　　|　　　　　　! 　 ||
　　　　　　|　　　 │　　　　|
　　　　　|　　　　| 　　| |
　　　　　| 　　　　　|　　　| |
　　　　 | 　　　　　 !　　　| |

**１３２人目の素数さん** · 2015/01/25(日) 19:37:01.31

Coq の論理的バックグラウンド（？）になってる
Calculus of Inductive Construction (CIC)
（？：何種類かあって良く分からない）
について調べたいのですが良い文献ないですか？

**１３２人目の素数さん** · 2015/01/25(日) 19:45:30.26

仕様記述言語Zとの関聯はないの？

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 16:34:55.90

自然数の範囲では、>>18は証明できないよ。
整数か実数か複素数を使わないと。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 17:08:56.67

Require Import Arith.
Require Import Omega.
Open Scope Z_scope.
Theorem t: forall n:Z, n*n - 2*n + 1 = (n-1)*(n-1).
intros.
symmetry.
replace ((n-1)*(n-1)) with (n*(n-1)-1*(n-1)).
replace (1*(n-1)) with (n-1).
replace (n*(n-1)) with (n*n-n).
replace (n*n-n-(n-1)) with (n*n-(n-1)-n).
replace (n*n-(n-1)) with (n*n-n+1).
replace (n*n-n+1-n) with (n*n-n-n+1).
replace (n*n-n-n) with (n*n-2*n).
omega.
omega.
omega.
omega.
omega.
symmetry.
replace (n*n-n) with (n*n-n*1).
apply Z.mul_sub_distr_l.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 17:13:27.24

Require Import Omega.
Open Scope Z_scope.
の後で
SearchAbout Z.するとZの定義が見られるからね。

**１３２人目の素数さん** · 2015/01/27(火) 19:50:17.70

>>26
俺の環境だと証明が通らないんだが。
なんかミスってない？

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 20:07:13.17

>>26
訂正。ガラケーで入力大変。

(誤)
apply Z.mul_sub_distr_l.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.

(正)
apply Z.mul_sub_distr_l.
omega.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 20:10:46.94

お題：
「３の倍数に６を足したものは３の倍数である」を証明せよ。

**１３２人目の素数さん** · 2015/01/27(火) 20:19:16.49

>>29
通った。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 20:27:34.17

>>24
聞いた覚えはないな

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 20:35:45.19

>>30

「xは３の倍数である」
⇔
∃y∈Ｚに対して「x＝3y」、

だな。１階述語とexistsを使って解いてくれ。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 20:59:02.99

例えば、
Definition trimul (n:nat) := exists m:nat, n = 3*m.
と定義すればtrimul(0)は次のように証明できる。
Theorem tmzero: trimul(0).
unfold trimul.
exists 0.
auto.
Qed.

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 21:17:44.23

>>30

Require Import Arith.
Require Import Omega.
Open Scope Z_scope.
Definition trimul (x:Z) := exists y:Z, x = 3*y.
Theorem t: forall x:Z, trimul(x) -> trimul(x+6).
intros.
unfold trimul.
destruct H.
exists (x0+2).
replace (x) with (3*x0).
omega.
Qed.

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 21:25:18.31

「Reset Initial.」コマンドでCoqを初期状態へ戻すことができる。
「unfold x.」はゴールにあるxをその定義に展開するタクティクだ。
「destruct H.」はHを崩すタクティク。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 21:30:41.25

お題：
「３の倍数に４を掛けたものは６の倍数である」を証明。

**１３２人目の素数さん** · 2015/01/27(火) 21:32:30.82

片山さん結構勉強進んでるな。

**１３２人目の素数さん** · 2015/01/27(火) 21:52:51.06

こう？

Require Import Omega.
Require Import Arith.
Open Scope Z_scope.

Definition tr(x:Z) := exists y:Z , x=3*y.
Definition s(x:Z) := exists y:Z,x=6*y.

Theorem t: forall x:Z,tr(x)->s(4*x).

intros.
unfold s.
destruct H.
exists (2*x0).
replace x with (3*x0).
omega.
Qed.

多分このスレには片山さんと俺しかいないぞｗ

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/27(火) 22:12:11.97

>>39
正解！

このスレを立てた目的は…
１．Coqの知名度アップと啓蒙。
２．Coqによる「片山QZの定理」の証明。
３．Coqと人工知能の連携を考えること。

**１３２人目の素数さん** · 2015/01/28(水) 08:18:03.12

>３．Coqと人工知能の連携を考えること。
ここをもう少し詳しく

**１３２人目の素数さん** · 2015/01/28(水) 18:28:09.93

どのお題も超簡単なものだけに見えるのだが、それはなぜ？
Coqでの証明法がだれにも分かりやすくなるようあえて題材は
簡単なものを選んでいるの？
もっとCoqの強力さが分かる位難しい題材でやってくれんかな。
そもそもCoqではどの位難しいものがどの位の手間で証明できるの？

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/28(水) 18:52:58.11

>>41
単純に言えば、コンピューターでできた数学者を作ろうとしている。
数学の問題は、式の変形と問題の分解と解の探索の問題に還元されるから、
人工知能でもいくつかの問題を解くことができるはずだ。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/28(水) 18:58:35.37

>>42
はじめは基礎と慣れが大事。不満なら君も出題してもかまわない。
次は集合論から出題したまえ。

**１３２人目の素数さん** · 2015/01/28(水) 19:12:43.24

>>44
なぜ集合論？
一応念のためいっとくが>>42は某スレの1(俺)とは別人だぞ。

**片山博文MZ** ◆T6xkBnTXz7B0 · 2015/01/28(水) 19:42:58.51

お題：
「Z⊆XかつZ⊆YならばZ⊆X∩Y」を証明せよ。

**１３２人目の素数さん** · 2015/01/28(水) 20:04:26.42

>>43
Coqあるいは片山さんは、東大ロボプロジェクトはどう評価してるの？

**１３２人目の素数さん** · 2015/01/28(水) 20:07:20.02

>>44
集合問題でなく整数問題の系統だが、まずはこういう易しめのお題はどう？
お題：正整数m、nがあり、LCM(m,n) + GCD(m,n) = m + n とする。
このとき、m, n のどちらか一方は、他方によって割り切れることを示せ。

**１３２人目の素数さん** · 2015/01/28(水) 22:31:29.58

易しいっていうけど>>48は>>48の証明をCoqでできるの？

**１３２人目の素数さん** · 2015/01/29(木) 09:57:12.57

俺はCoqのド素人だから聞いてる。
だが人間にとって証明問題といえばふつうこれくらいからだろ？

**１３２人目の素数さん** · 2015/01/30(金) 10:46:00.89

☆☆☆☆☆
☆ 自民党、グッジョブですわ。 ☆
http://www.soumu.go.jp/senkyo/kokumin_touhyou/index.html

☆ 日本国民の皆様方、2016年7月の『第24回参議院選挙』で、改憲の参議院議員が
3分の2以上を超えると日本国憲法の改正です。皆様方、必ず投票に自ら足を運んでください。
そして、私たちの日本国憲法を絶対に改正しましょう。☆