2ちゃんねる スマホ用 ■掲示板に戻る■ 全部 1- 最新50    

■ このスレッドは過去ログ倉庫に格納されています

【Coq】コンピューターで証明しよう【コック】

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

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

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

2 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 01:51:30.31 ID:kQ1pk3tS.net
自然数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.

3 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 01:56:25.68 ID:kQ1pk3tS.net
自然数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.

4 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 02:10:51.92 ID:kQ1pk3tS.net
Coqは証明支援システムです。数学論文を英語で書ける程度の素養が必要です。
まずはTutorialを読むことから始めましょう。
natは自然数(natural numbers)の略です。
Coqでは英語や英語の略語がよく使われます。

5 :132人目の素数さん:2015/01/23(金) 13:44:42.12 ID:xOpKLzij.net
自動的に証明ができるんじゃないだろ
そこんとこ誤解させんなよ

6 :132人目の素数さん:2015/01/23(金) 13:50:52.34 ID:v4GbgrUP.net
       ____
     /⌒  ⌒\
   /  癶   癶 \
  /::::::⌒(__人__)⌒::::: \   あらあらうふふ
  |     |r┬-|     |
  \      `ー'´     /

7 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 16:34:52.63 ID:kQ1pk3tS.net
>>5
すみません。

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

8 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 16:42:51.44 ID:kQ1pk3tS.net
「Require Import Arith.」は、
「Arith」というモジュール(部品)を読み込むコマンドだ。
コマンド「Theorem t: forall n:nat, 2*n = n+n.」について。
「Theorem t:」は、これから「t」という名前の定理を証明するよって意味。
「forall n:nat,」は、「∀n∈N」という意味。
ここで「∀」は論理学における「任意の…に対して」という意味。
「∈」は集合論の「…に属する」に相当する。

9 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 16:48:37.07 ID:kQ1pk3tS.net
掛け算について現在の定義を調べたいなら、掛け算の略は「mult」だから、「SearchAbout mult.」というコマンドを入力すればいい。
自然数について調べたいなら「SearchAbout nat.」を入力。
足し算なら「SearchAbout plus.」。

10 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 16:57:07.60 ID:kQ1pk3tS.net
Theoremコマンドを入力したら、証明モードに入る。
証明モードでは、証明するための「タクティク」(戦術)を入力できる。
コマンドは大文字で始まるが、タクティクは小文字で始まる。
タクティクの例を挙げると、intros,symmetry,left,right,auto,elim,applyなど、いろんなタクティクがある。
証明の終わりでは「Qed.」コマンドを入力する。

11 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 17:12:06.01 ID:kQ1pk3tS.net
さて、Coqのダウンロードとインストールが終わったら、早速Coqを起動しよう。
黒い画面に「Coq <」と表示されるだろう。
これはCoqのプロンプトであり、入力待ちであることを表している。

12 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/23(金) 17:15:42.51 ID:kQ1pk3tS.net
Coqの終了コマンドは「Quit.」である。「Quit.」と打ち込んでEnterキーを押せば
黒い画面が消えるであろう。

13 :132人目の素数さん:2015/01/23(金) 21:55:31.77 ID:bh227Vy0.net
suck my coq!

14 :132人目の素数さん:2015/01/23(金) 23:54:02.33 ID:WDVlZtXn.net
まずは1がなんかお題だせよ。

15 :132人目の素数さん:2015/01/24(土) 00:15:52.39 ID:G4KHuvpv.net
Coqは数学、プログラミング両方で高い水準を要求されるからな。
このスレは人集まらないだろう。
数板ではプログラムの素養がネックになるか?

16 :132人目の素数さん:2015/01/24(土) 00:29:02.73 ID:w9MHCKHx.net
証明支援系のプログラムにバグがないことはどうやって
証明するの?

17 :132人目の素数さん:2015/01/24(土) 08:29:32.31 ID:jovcH18s.net
meta coqを使いなさい

18 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/24(土) 09:04:43.49 ID:9w/8qlKh.net
お題:
x^2 - 2x + 1 = (x - 1)^2の証明。

19 :132人目の素数さん:2015/01/24(土) 13:04:41.68 ID:Wn9XFPkK.net
>>15
いやいや、いいスレだ。せいぜい集まろうぜ

20 :132人目の素数さん:2015/01/24(土) 17:26:49.57 ID:G4KHuvpv.net
-を+に変えた版はできた。
-の方はまだできてない。

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.

21 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/24(土) 20:21:46.13 ID:9w/8qlKh.net
>>20
もう少しだな。-2x=+(-2)xを使えば、できるはずだ。

22 :132人目の素数さん:2015/01/24(土) 22:01:32.97 ID:WXgNhwIy.net
        /⌒ヽ⌒ヽ
               Y
            八  ヽ
     (   __//. ヽ,, ,)
      丶1    八.  !/
       ζ,    八.  j
        i    丿 、 j
        |     八   |
        | !    i 、 |
       | i し " i   '|
      |ノ (   i    i|
      ( '~ヽ   !  ‖
        │     i   ‖
      |      !   ||
      |    │    |
      |       |    | |
     |       |   | |
     |        !    | |

23 :132人目の素数さん:2015/01/25(日) 19:37:01.31 ID:4ki3LVZe.net
Coq の論理的バックグラウンド(?)になってる
Calculus of Inductive Construction (CIC)
(?:何種類かあって良く分からない)
について調べたいのですが良い文献ないですか?

24 :132人目の素数さん:2015/01/25(日) 19:45:30.26 ID:HYD7R+Gz.net
仕様記述言語Zとの関聯はないの?

25 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 16:34:55.90 ID:SJxzPcnV.net
自然数の範囲では、>>18は証明できないよ。
整数か実数か複素数を使わないと。

26 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 17:08:56.67 ID:SJxzPcnV.net
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.

27 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 17:13:27.24 ID:SJxzPcnV.net
Require Import Omega.
Open Scope Z_scope.
の後で
SearchAbout Z.するとZの定義が見られるからね。

28 :132人目の素数さん:2015/01/27(火) 19:50:17.70 ID:BM4PDVdL.net
>>26
俺の環境だと証明が通らないんだが。
なんかミスってない?

29 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 20:07:13.17 ID:SJxzPcnV.net
>>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.

30 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 20:10:46.94 ID:SJxzPcnV.net
お題:
「3の倍数に6を足したものは3の倍数である」を証明せよ。

31 :132人目の素数さん:2015/01/27(火) 20:19:16.49 ID:BM4PDVdL.net
>>29
通った。

32 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 20:27:34.17 ID:SJxzPcnV.net
>>24
聞いた覚えはないな

33 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 20:35:45.19 ID:SJxzPcnV.net
>>30

「xは3の倍数である」

∃y∈Zに対して「x=3y」、

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

34 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 20:59:02.99 ID:SJxzPcnV.net
例えば、
Definition trimul (n:nat) := exists m:nat, n = 3*m.
と定義すればtrimul(0)は次のように証明できる。
Theorem tmzero: trimul(0).
unfold trimul.
exists 0.
auto.
Qed.

35 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 21:17:44.23 ID:SJxzPcnV.net
>>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.

36 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 21:25:18.31 ID:SJxzPcnV.net
「Reset Initial.」コマンドでCoqを初期状態へ戻すことができる。
「unfold x.」はゴールにあるxをその定義に展開するタクティクだ。
「destruct H.」はHを崩すタクティク。

37 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 21:30:41.25 ID:SJxzPcnV.net
お題:
「3の倍数に4を掛けたものは6の倍数である」を証明。

38 :132人目の素数さん:2015/01/27(火) 21:32:30.82 ID:BM4PDVdL.net
片山さん結構勉強進んでるな。

39 :132人目の素数さん:2015/01/27(火) 21:52:51.06 ID:BM4PDVdL.net
こう?

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.

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

40 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/27(火) 22:12:11.97 ID:SJxzPcnV.net
>>39
正解!

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

41 :132人目の素数さん:2015/01/28(水) 08:18:03.12 ID:Q7XfmRRj.net
>3.Coqと人工知能の連携を考えること。
ここをもう少し詳しく

42 :132人目の素数さん:2015/01/28(水) 18:28:09.93 ID:Q7XfmRRj.net
どのお題も超簡単なものだけに見えるのだが、それはなぜ?
Coqでの証明法がだれにも分かりやすくなるようあえて題材は
簡単なものを選んでいるの?
もっとCoqの強力さが分かる位難しい題材でやってくれんかな。
そもそもCoqではどの位難しいものがどの位の手間で証明できるの?

43 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/28(水) 18:52:58.11 ID:xr03hxaD.net
>>41
単純に言えば、コンピューターでできた数学者を作ろうとしている。
数学の問題は、式の変形と問題の分解と解の探索の問題に還元されるから、
人工知能でもいくつかの問題を解くことができるはずだ。

44 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/28(水) 18:58:35.37 ID:xr03hxaD.net
>>42
はじめは基礎と慣れが大事。不満なら君も出題してもかまわない。
次は集合論から出題したまえ。

45 :132人目の素数さん:2015/01/28(水) 19:12:43.24 ID:MQBQj2T8.net
>>44
なぜ集合論?
一応念のためいっとくが>>42は某スレの1(俺)とは別人だぞ。

46 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/28(水) 19:42:58.51 ID:xr03hxaD.net
お題:
「Z⊆XかつZ⊆YならばZ⊆X∩Y」を証明せよ。

47 :132人目の素数さん:2015/01/28(水) 20:04:26.42 ID:Q7XfmRRj.net
>>43
Coqあるいは片山さんは、東大ロボプロジェクトはどう評価してるの?

48 :132人目の素数さん:2015/01/28(水) 20:07:20.02 ID:Q7XfmRRj.net
>>44
集合問題でなく整数問題の系統だが、まずはこういう易しめのお題はどう?
お題:正整数m、nがあり、LCM(m,n) + GCD(m,n) = m + n とする。
このとき、m, n のどちらか一方は、他方によって割り切れることを示せ。

49 :132人目の素数さん:2015/01/28(水) 22:31:29.58 ID:MQBQj2T8.net
易しいっていうけど>>48>>48の証明をCoqでできるの?

50 :132人目の素数さん:2015/01/29(木) 09:57:12.57 ID:rxXHbRm8.net
俺はCoqのド素人だから聞いてる。
だが人間にとって証明問題といえばふつうこれくらいからだろ?

51 :132人目の素数さん:2015/01/30(金) 10:46:00.89 ID:NnXyGTxc.net
☆☆☆☆☆
☆ 自民党、グッジョブですわ。 ☆
http://www.soumu.go.jp/senkyo/kokumin_touhyou/index.html

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

52 :132人目の素数さん:2015/01/30(金) 11:16:04.23 ID:UCtzINaz.net
>>23

53 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/31(土) 11:42:47.03 ID:HFUS6FCH.net
>>48
http://ideone.com/Aa07zr

「Z.lcm m n = m0 * n0 * Z.gcd m n」の証明が難しい。

54 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/31(土) 11:48:29.43 ID:HFUS6FCH.net
「Coqにおける集合論的直観主義数学の実装」
名古屋大学 佐藤雅大さん
http://shirodanuki.cs.shinshu-u.ac.jp/TPP/TPP2013_satou.pdf

55 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/31(土) 12:04:50.95 ID:HFUS6FCH.net
https://coq.inria.fr/distrib/current/files/
からTutorial.pdfとReference-Manual.pdfとrefman.tar.gzを
ダウンロードすること。

56 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/31(土) 12:21:52.24 ID:HFUS6FCH.net
stdlib.tar.gzもダウンロードすること。

57 :132人目の素数さん:2015/01/31(土) 14:08:26.29 ID:2+EKWeFU.net
>>53
まじめにやってくれてサンクス。
それで
>http://ideone.com/Aa07zr
これはすべて人が書いてるんだね? だとするとメリットがわからんな。
「コンピュータを使って定理証明する」て、人が形式証明を計算機に打ち込む
ということか?ふつうはそれとは違う意味で言うことだが。

58 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/31(土) 15:43:01.36 ID:frnU9ywC.net
>>57
それは私が書きました。

59 :132人目の素数さん:2015/01/31(土) 16:38:52.37 ID:53IzKqnQ.net
直観主義的でない非構成的な手続きも扱えるの?

60 :片山博文MZ ◆T6xkBnTXz7B0 :2015/01/31(土) 16:51:07.75 ID:frnU9ywC.net
>>59
Classicalモジュールを使えばね

61 :132人目の素数さん:2015/01/31(土) 18:21:07.36 ID:2+EKWeFU.net
>>58
東大ロボは>>48くらいは当然自動で解くんだがね

62 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/01(日) 23:27:39.12 ID:/+/CiuQP.net
>>46ができたヤツは居ないか?

63 :132人目の素数さん:2015/02/02(月) 20:07:15.55 ID:yNmPHm6y.net
>>46チャレンジしようとして集合のモジュール名がわからなくて投げた俺が通りますよ。

64 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/02(月) 20:37:51.75 ID:REXIs8D3.net
モジュール名はstdlibに書かれてあるはずだが。

65 :132人目の素数さん:2015/02/02(月) 21:22:28.59 ID:yNmPHm6y.net
stdlib落としてなかったわ。スマソ

66 :132人目の素数さん:2015/02/02(月) 21:41:32.43 ID:yNmPHm6y.net
stdlib読んでも意味わかんなかった俺が通りますよw
Ensemblesってのでいいのか?
そこからわからんw

67 :132人目の素数さん:2015/02/02(月) 22:26:56.55 ID:yNmPHm6y.net
じっくり読むとなんとなくわかってくるな。
もうちょっとやってみるわ

68 :132人目の素数さん:2015/02/02(月) 23:16:26.32 ID:yNmPHm6y.net
Included Z XのZとXって同じ型じゃいかんの?
よくわからぬ。

69 :132人目の素数さん:2015/02/03(火) 06:16:35.66 ID:AsZmhMLH.net
支援age
自動定理証明器の設計の話題にまで広がりますように

70 :132人目の素数さん:2015/02/03(火) 06:21:09.41 ID:AsZmhMLH.net
(・ω・)

71 :132人目の素数さん:2015/02/03(火) 11:39:09.23 ID:TF0+kICu.net
>>69
賛成かな? 
ただ俺の場合は、Coqの細かい話はうんざりだ。単なる証明支援の今のCoqなら将来はないんだから。
早く自動証明の話をしてくれ

72 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/03(火) 17:56:27.70 ID:lc3NHdIs.net
Coq自体は、関数型言語として有名なOCamlで記述されている。
Coqのソースコードは同じ場所でダウンロードできる。
自動証明を行いたいなら、Omegaのようなモジュールを自作するか、
Coqを改造するか、Coqと対話する必要がある。

73 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/03(火) 18:12:57.83 ID:lc3NHdIs.net
最新のソースコードcoq-8.4pl5.tar.gzをダウンロードし、解凍ソフトLhaplusなどを使って解凍(展開)すると、
coq-8.4pl5というフォルダーができる。
ここにパスcoq-8.4pl5/plugins/omega/にOmegaが記述されている。
ファイルの中身はテキストエディターなどで確認できる。

74 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/03(火) 20:37:43.72 ID:lc3NHdIs.net
過去スレでよければ

Coqスレ
http://peace.2ch.net/test/read.cgi/tech/1300017923/

75 :132人目の素数さん:2015/02/04(水) 10:08:30.01 ID:cf1lNhgP.net
> 自動証明を行いたいなら、Omegaのようなモジュールを自作するか、
> Coqを改造するか、Coqと対話する必要がある。
Coqの延長でできる風に言ってるが、それはもうCoqではないだろう

76 :132人目の素数さん:2015/02/04(水) 12:44:57.04 ID:ii+fPoPp.net
人工知能の進歩を見てると、やはり半端ない多量の証明のデータの蓄積をした上で、それをコンピュータ自身が分析し、与えられた定理にはどのような手法が適している可能性が高いかを推測するようなシステムになるのかな。
人間も結局過去の膨大な証明から経験的に学んでるわけだし。

77 :132人目の素数さん:2015/02/04(水) 15:13:34.03 ID:RvZcFYHN.net
定石データベースが必要

78 :132人目の素数さん:2015/02/04(水) 21:09:33.67 ID:ZZSly8gS.net
Coqが証明できる定理ってなにか制限あるの?
それとも人間が証明できる定理は原理的にCoqでも証明できる?

79 :132人目の素数さん:2015/02/04(水) 22:19:29.39 ID:cf1lNhgP.net
>>78
Coqはなにも証明しない!人間が証明してる。Coqは証明用ワープロ

80 :132人目の素数さん:2015/02/04(水) 23:26:04.49 ID:GsyGT2Ng.net
>>79
えっ、正しい論証になってるかチェックしてくれないの?

81 :132人目の素数さん:2015/02/05(木) 19:10:49.09 ID:iuUfy0y0.net
コンパイラも文法チェックはするが、コンパイラがプログラミングしてるとは言わんだろ

82 :132人目の素数さん:2015/02/05(木) 19:25:35.41 ID:vIbaBBBO.net
コンピュータにも分かるように証明書くのが一苦労だわ

83 :132人目の素数さん:2015/02/05(木) 19:29:39.63 ID:160T3VWS.net
ランダム生成やってみれば

84 :132人目の素数さん:2015/02/05(木) 19:53:49.21 ID:RkehamlL.net
メモリいっぱい積んで幅優先でやってみたいね。
すぐメモリたんなくなるだろうけど。

85 :132人目の素数さん:2015/02/05(木) 20:23:32.85 ID:iuUfy0y0.net
>>82
一苦労どころじゃないだろw
このスレッドを見ても、ほとんど定義そのもの程度の命題の証明がお題になるくらいだからな

86 :132人目の素数さん:2015/02/06(金) 10:38:19.60 ID:p5z+W0p1.net
CICのnormalization theoremを証明してあるわかりやすい文献教えてくらはい、えらいひと。

87 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/08(日) 17:07:42.20 ID:6NKOGxqa.net
お題:中国剰余定理を証明せよ。

88 :132人目の素数さん:2015/02/08(日) 21:00:27.66 ID:SqIZWWvP.net
ロボコックに料理させよう

89 :132人目の素数さん:2015/02/09(月) 05:48:38.91 ID:M8cSVEsc.net
キャメルとかいう言語も勉強したほうがいいのでしょうか?

90 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/10(火) 11:43:05.83 ID:kDD4UbcZ.net
>>89
OCamlな。
Coqの動作原理を知りたいならOCamlで書かれたCoqのソースとにらめっこ

91 :132人目の素数さん:2015/02/10(火) 20:43:52.91 ID:0p3zZ1nn.net
Coqのソースとか何万ステップあんのよ?

92 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/10(火) 21:23:49.89 ID:kDD4UbcZ.net
>>91
心臓部を理解すれば後は枝葉

93 :132人目の素数さん:2015/02/10(火) 21:29:15.74 ID:0p3zZ1nn.net
>>92
心臓部とか何ステップくらいなのよ?

94 :132人目の素数さん:2015/02/10(火) 21:31:54.68 ID:HSrgtPR2.net
個人でいきなり読みにいってもきっと読めないんでしょ?
数学の本スレでちょっと前に誰かが聞いて、
経験者らしきそっちの学識ありそうな誰かが応えてた
自動定理証明器の古典本あたりから読まないと・・・

勉強会とかするなら参加したいわ

95 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/11(水) 07:12:51.62 ID:Dr+1DDR1.net
数学の体系は、公理系によって成り立っている。すなわち、
当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、
さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。
そのように数学は、間違いのない証明によって次々と築き上げるものである。

96 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/11(水) 07:20:21.76 ID:Dr+1DDR1.net
証明に1つでも間違いがあれば、公理系は崩壊する。間違いが1つでも紛れ込めば、
どんな命題でも証明可能になり、証明が無意味となる。

97 :132人目の素数さん:2015/02/11(水) 07:36:02.60 ID:v8Hqr9Iu.net
なにかの新書のキャッチコピーか?

98 :132人目の素数さん:2015/02/11(水) 09:29:50.38 ID:j/Krena0.net
>>95 >>96
なにを言いたい?
なお、証明が間違っていても公理系は崩壊しないw

99 :132人目の素数さん:2015/02/11(水) 10:23:15.61 ID:dm165ELq.net
スレ主に正直ガッカリ感
この船頭では…

100 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/11(水) 10:48:45.59 ID:Dr+1DDR1.net
>>98
公理の集合のことを公理系って言うんだったね。
よって>>95-96は間違い。

101 :132人目の素数さん:2015/02/11(水) 14:50:41.92 ID:YQf1vLE3.net
スレ主の精神が崩壊

102 :132人目の素数さん:2015/02/11(水) 16:30:07.99 ID:cuKCaaA+.net
>>86

103 :132人目の素数さん:2015/02/11(水) 20:46:57.00 ID:H06TaWd8.net
>>101
それは前から分かっていること

104 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/13(金) 02:36:25.72 ID:4T+ZQiA6.net
同値変換だけで命題論理式を最も単純な節形式にするって未解決だよな?

105 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/13(金) 13:45:35.78 ID:Zi/5tAa8.net
クワイン・マクラスキー法
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

106 :片山博文MZ ◆T6xkBnTXz7B0 :2015/02/13(金) 17:47:55.74 ID:4T+ZQiA6.net
NP困難なんて気合いと悪運で突破する!

107 :132人目の素数さん:2015/02/13(金) 20:56:57.57 ID:Wb77hhv6.net
せめて近似で突破して

108 :132人目の素数さん:2015/02/16(月) 06:52:55.96 ID:eGQOGV7p.net
私、O'Camlなどでのプログラミング経験はあるが数学の力に自信がないもので、数学書を一人で読み進める時にきちんと証明出来ている確信が欲しくて久しぶりにCoqを触り始めました。
証明のコードを生成してみるのもまた愉し。

109 :132人目の素数さん:2015/02/16(月) 11:44:48.02 ID:OK+Cd/WQ.net
>>86もう無理でしょうか。しくしく。

110 :132人目の素数さん:2015/02/16(月) 19:45:39.73 ID:46V2KXPR.net
Coqってグッドスタイン数列の収束は証明できるの?

111 :132人目の素数さん:2015/03/17(火) 05:27:20.77 ID:SwDWqZM9.net
検証はイメージできるけど証明か

112 :132人目の素数さん:2015/03/17(火) 11:09:06.79 ID:p3znTvh+.net
検証と証明ってどう違うの
一例の場合か全ての場合かってこと?

113 :132人目の素数さん:2015/03/17(火) 12:42:17.91 ID:SwDWqZM9.net
具体的に人間が与えた証明が正しい推論になっているか確かめるのが検証。
証明システムなら人工知能が結論までの道筋を自ら見つけるということになるはず。

114 :132人目の素数さん:2015/03/17(火) 21:53:44.21 ID:sQPcb9ll.net
Coqって順序数扱えんの?

115 :132人目の素数さん:2015/03/19(木) 15:02:35.75 ID:g9YALw9l.net
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に変える命令とかあるんでしょうか?

116 :追加:2015/03/19(木) 15:03:19.56 ID:g9YALw9l.net
ちなみに、
Proof.
intros x a.
unfold mu.
intros P b.
apply b.
apply (m mu P).
intros x0 y.
apply y.
までが上記の結果です。

117 :132人目の素数さん:2015/03/23(月) 21:55:09.34 ID:hFhIEEUk.net
>>95
>数学の体系は、公理系によって成り立っている。すなわち、
>当たり前の真実である「公理(axiom)」の集合から「定理(theorem)」を証明により導出し、
>さらに既存の公理の集合と、証明された定理の集合から導出された、新しい定理をさらに土台とする。
>そのように数学は、間違いのない証明によって次々と築き上げるものである。

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

118 :132人目の素数さん:2015/04/13(月) 14:47:42.65 ID:gEnxmz80.net
ここは死んでしまったのでしょうか。しくしく。

119 :片山博文MZ ◆T6xkBnTXz7B0 :2015/04/13(月) 16:42:48.12 ID:oOocMLFA.net
すまね。仕事で忙しい、疲れてるときは数学ができない。

120 :132人目の素数さん:2015/04/13(月) 19:17:53.26 ID:SKfHu0g2.net
景気いいの?
浦山

121 :132人目の素数さん:2015/04/17(金) 21:21:52.45 ID:oyQOgKjs.net
>>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.

122 :132人目の素数さん:2015/04/17(金) 22:20:53.23 ID:KzUa3HIJ.net
((p∧q)→r)→((p→r)∨(q→r))
は証明できますか

123 :132人目の素数さん:2015/04/18(土) 09:18:54.32 ID:Q1uVLxMU.net
直観主義では証明できないので
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.

124 :132人目の素数さん:2015/04/18(土) 10:22:46.84 ID:Q1uVLxMU.net
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.

125 :132人目の素数さん:2015/04/18(土) 11:34:32.18 ID:Q1uVLxMU.net
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.

126 :115:2015/04/18(土) 16:08:27.46 ID:Ch74qrhJ.net
>>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
で古いのでしょうか。

127 :122:2015/04/18(土) 18:57:48.32 ID:CUF6Decr.net
>>123-125
ありがとうございます。
知らなったタクティクがいっぱいありますね。

128 :132人目の素数さん:2015/04/19(日) 20:01:47.33 ID:wQv7TFhy.net
>>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.

129 :115:2015/04/21(火) 16:23:18.95 ID:X1phHP6G.net
>>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な変数が原因であることがわかりました。

130 :129:2015/04/21(火) 16:25:47.49 ID:X1phHP6G.net
そこで、次のように証明手順を変えてみると、なんと、最期の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.

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

131 :132人目の素数さん:2015/04/24(金) 23:44:49.27 ID:RQUiSeMS.net
@eq Set a b と @eq Type a b は違う型なのが原因な気がする。
130のようなQedでエラーになるのは結構あって、証明モードの途中ではあんまり頑張って型検査しないから、
こういう微妙な型の差しかないときはしかたないかな。

132 :129:2015/04/29(水) 09:13:55.74 ID:Z8S8LZWA.net
レス大感謝です。結局は反則をすることによって解決しました。つまり、
証明法を探すのではなく、>>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.

133 :132人目の素数さん:2015/04/29(水) 21:07:39.24 ID:DcI2ISH9.net
Coqで作られたCコンパイラがあるそうですが、
詳しいことがわかるURLないでしょうか。

134 :132人目の素数さん:2015/04/29(水) 21:13:19.95 ID:mzyslicl.net
>>133
http://compcert.inria.fr/compcert-C.html

135 :133:2015/04/30(木) 11:12:49.99 ID:YN5jSrOT.net
ありがとうございます。
読んでみます。

136 :片山博文MZ ◆T6xkBnTXz7B0 :2015/05/05(火) 22:36:38.53 ID:4exTCqPC.net
>>134
こりゃすげーや

137 :132人目の素数さん:2015/05/06(水) 11:27:30.01 ID:EJxZqkF+.net
なにがどうすごいのか3行でplz

138 :132人目の素数さん:2015/05/17(日) 09:28:41.49 ID:Qam78Q26.net
Cock!

139 :132人目の素数さん:2015/05/29(金) 21:19:13.70 ID:sppsbb3D.net
Coqだと停止しないコードは書けないそうですが、
停止するコードは必ずCoqでも等価なコードがかけるのかどうか気になります。
書けるんでしょうか?

140 :132人目の素数さん:2015/06/01(月) 20:03:21.42 ID:vP0/D1Ed.net
停止するかどうかわかるということは停止までのステップ数も見積もれるんでしょうか。
大まかでいいので。

141 :132人目の素数さん:2015/06/17(水) 02:15:51.60 ID:w70GpJG/.net
Coqそのものの話じゃなくてすいませんが、software foundationsと言うCoqの解説書↓
http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

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

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

142 :132人目の素数さん:2015/06/19(金) 00:07:06.67 ID:KgdfsOzM.net
>>140
このライブラリを使えばいいんじゃないかな、
https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html

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

143 :141:2015/06/21(日) 09:25:51.67 ID:szLD4AMj.net
make all.pdfした時に実行されるcoqdepの出力が逆順になっているので、
これをシェルスクリプトで逆順にしたら、それらしい順番のPDFになりました。
書き忘れましたが、使ってた環境はcoq 8.4pl6です。
お騒がせしました

144 :132人目の素数さん:2015/06/23(火) 19:05:42.67 ID:y39xeCDy.net
>>142
返信遅れてすいません。
読んでもよく理解できないTT

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

145 :132人目の素数さん:2015/10/14(水) 23:33:20.11 ID:kbKTDEnq.net
数蝉

146 :132人目の素数さん:2015/11/02(月) 15:40:58.39 ID:voHQlbVG.net
数学セミナーvol.54 no.11 649
特集 コンピュータにできる数学・できない数学
 Coq:型理論から来た証明支援系, Jacques Garrigue

147 :132人目の素数さん:2016/05/25(水) 19:39:54.39 ID:EB6pp118.net
質問よろしいでしょうか。
「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」となって、証明できません。
お知恵を貸していただけないでしょうか……

148 :132人目の素数さん:2016/05/25(水) 20:46:14.27 ID:EofZeTbn.net
まずはこれを解いてみるとか。

Require Import Omega.

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

149 :132人目の素数さん:2016/05/25(水) 20:55:32.32 ID:EofZeTbn.net
俺の環境じゃ以下のもOmega解いてくれなかったわ。なぜ?

Theorem t:
2^10 > 1000.

150 :132人目の素数さん:2016/05/25(水) 23:04:16.75 ID:EB6pp118.net
僕の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.

151 :132人目の素数さん:2016/05/25(水) 23:09:57.26 ID:EofZeTbn.net
simplとやらがカギなのか?
元の問題にもsimpl使えない?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

169 :132人目の素数さん:2016/07/06(水) 11:09:19.26 ID:udLxg5Zs.net
夏 休 み の 友
http://gathery.recruit-lifestyle.co.jp/article/1146775541637910801

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

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

172 :片山博文MZ ◆T6xkBnTXz7B0 :2016/07/08(金) 23:48:26.99 ID:V/uvjwWo.net
>>171
http://proofweb.cs.ru.nl/install.php

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

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

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


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

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


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



178 ::2017/06/18(日) 17:51:22.79 ID:ze+BLRMV.net


179 ::2017/06/18(日) 17:51:43.36 ID:ze+BLRMV.net


180 ::2017/06/18(日) 17:52:04.31 ID:ze+BLRMV.net


181 ::2017/06/18(日) 17:52:25.55 ID:ze+BLRMV.net


182 ::2017/06/18(日) 17:52:46.45 ID:ze+BLRMV.net


183 ::2017/06/18(日) 17:53:06.29 ID:ze+BLRMV.net


184 ::2017/06/18(日) 17:53:32.46 ID:ze+BLRMV.net


185 ::2017/06/18(日) 17:53:52.62 ID:ze+BLRMV.net


186 ::2017/06/18(日) 17:54:12.00 ID:ze+BLRMV.net


187 ::2017/06/18(日) 17:54:31.69 ID:ze+BLRMV.net


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

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

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



191 ::2017/06/19(月) 07:24:06.41 ID:pqzlCEdf.net


192 ::2017/06/19(月) 07:24:23.72 ID:pqzlCEdf.net


193 ::2017/06/19(月) 07:24:43.20 ID:pqzlCEdf.net


194 ::2017/06/19(月) 07:25:01.34 ID:pqzlCEdf.net


195 ::2017/06/19(月) 07:25:18.52 ID:pqzlCEdf.net


196 ::2017/06/19(月) 07:25:36.12 ID:pqzlCEdf.net


197 ::2017/06/19(月) 07:25:54.24 ID:pqzlCEdf.net


198 ::2017/06/19(月) 07:26:18.53 ID:pqzlCEdf.net


199 ::2017/06/19(月) 07:26:35.36 ID:pqzlCEdf.net


200 ::2017/06/19(月) 07:26:54.38 ID:pqzlCEdf.net


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

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

203 :132人目の素数さん:2018/10/17(水) 09:46:19.60 ID:d5lKPIgu.net
数学者の定義しだい

204 :132人目の素数さん:2020/02/24(月) 04:56:39 ID:DY3MFCYd.net
>>7
> English speakerに前置きなく「コック」って言ったら誤解を産むよね
日本語話者にも開発者のCoquandの名前を「コカン」って呼んだら誤解生みそう

「Coqはコカンが生みました」

?????

205 :132人目の素数さん:2020/03/13(金) 02:15:49.03 ID:eeULFYX7.net
Coqのライブラリ集ってどう探しますか?

206 :132人目の素数さん:2020/04/08(水) 03:27:53 ID:/9nfhwXS.net
ggl

207 :132人目の素数さん:2020/04/28(火) 21:44:58 ID:5sXxAZXE.net
数学の教科書をcoqで翻訳して公開したら著作権違反になりますか?

208 :132人目の素数さん:2020/08/31(月) 18:29:37 ID:5YDNY7qe.net
これでMathematicaみたいなことができるの?

209 :132人目の素数さん:2020/08/31(月) 19:38:58.46 ID:CK4NnquJ.net
>>207
それは翻訳じゃなくて詳細な機械証明をつけたことになるからいいんじゃね?

やれるもんならやってごらん(挑発)

210 :132人目の素数さん:2020/09/01(火) 19:16:57.55 ID:2qjbTlF5.net
1700
学コン・宿題ボイコット実行委員会@gakkon_boycott 9月1日
#拡散希望
#みんなで学コン・宿題をボイコットしよう
雑誌「大学への数学」の誌上で毎月開催されている学力コンテスト(学コン)と宿題は、添削が雑で採点ミスが多く、訂正をお願いしても応じてもらえない悪質なコンテストです。(私も7月号の宿題でその被害に遭いました。)このようなコンテストに参加するのは時間と努力の無駄であり、参加する価値はありません。そこで私は、これ以上の被害者を出さないようにするため、また、出版社に反省と改善を促すために、学コン・宿題のボイコットを呼び掛けることにしました。少しでも多くの方がこの活動にご賛同頂き、このツイートを拡散して頂ければ幸いです。
https://twitter.com/gakkon_boycott/status/1300459618326388737
(deleted an unsolicited ad)

211 :132人目の素数さん:2020/12/29(火) 17:55:55.21 ID:dboOL2nl.net
>>209
ありがとうございます😊
やってみようと思います。

212 :132人目の素数さん:2020/12/29(火) 18:10:40.92 ID:L4ADUw+o.net
Coqとかのソフトウェアを理解して使えるようになるには,どんな本を読めばいいですか?

213 :132人目の素数さん:2020/12/29(火) 19:37:12.97 ID:dboOL2nl.net
本なら『Coq/SSReflect/MathCompによる定理証明』かな。実際に使って証明したいものを証明した方が良いと思うけど。

214 :132人目の素数さん:2020/12/29(火) 20:13:39.22 ID:L4ADUw+o.net
>>213
ありがとうございます.
その本は読んだことがあるのですが,何が書いてあるのかよくわかりませんでした.
その本を読むための予備知識はどんな本を読めばいいのでしょうか?

215 :132人目の素数さん:2020/12/29(火) 22:12:44.60 ID:dboOL2nl.net
Coqで何をしたいのかは分からないけど、数学の証明をしたいのなら命題論理とか述語論理の勉強をしたらいいと思うよ。

216 :132人目の素数さん:2020/12/30(水) 05:46:12.85 ID:8k4OPHBX.net
プログラムの観点から言うと、「依存型」「カリー=ハワード同型対応」がキーワードになるかな。
あんまり伸びてないけど、ム板にこういうスレがある。

【F*】依存型っていいの?【Coq】
https://mevius.5ch.net/test/read.cgi/tech/1554809503/

217 :132人目の素数さん:2021/03/04(木) 23:54:49.26 ID:5lNvn7IX.net
F x = If x < 10 then x else F (x - 1)

みたいな関数ってCoqでどう性質を証明しますか?ifの条件で場合分けしたいです

タクティックでcase ( x< 10)としても、
仮説にならないで、場合わけにならずに困っています。

218 :132人目の素数さん:2021/03/05(金) 08:47:36.61 ID:F3YWjIOX.net
>>217
はっきり見てないけど、こことか参考にならないかな?
https://stackoverflow.com/questions/16555022/proving-if-then-else-in-coq

219 :132人目の素数さん:2021/03/05(金) 09:33:07.21 ID:ACbQ1+Cx.net
>>218
まさにこれっぽいです。ありがとうございます!

220 :132人目の素数さん:2021/04/18(日) 19:19:36.97 ID:3tfcWKwp.net
Coqで日本語データを処理するプログラム書けますか?
Asciiは扱えるみたいです。

221 :132人目の素数さん:2021/06/13(日) 11:30:42.81 ID:yMfojtwc.net
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 => ?.

222 :132人目の素数さん:2021/06/13(日) 12:05:53.03 ID:lCrOJ5I2.net
>>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) の部分の括弧は外す事ができる。

223 :132人目の素数さん:2021/06/17(木) 19:16:48.45 ID:oqo44TQm.net
証明支援システムCoq、新しい名称を検討中
https://developers.srad.jp/story/21/06/16/1737205/

224 :132人目の素数さん:2022/01/12(水) 08:10:41.00 ID:0y6QDPS2.net
コックむずい

225 :132人目の素数さん:2022/01/24(月) 07:16:51.96 ID:OmUr/Vw+.net
ムズいよねえ
もっと勉強しなくては

226 :132人目の素数さん:2022/02/11(金) 01:30:20.50 ID:92XxvpJY.net
   | \
   |Д`) ダレモイナイ・・オドルナラ イマノウチ
   |⊂
   |


     ♪  Å
   ♪   / \   ランタ タン
      ヽ(´Д`;)ノ   ランタ タン
         (  へ)    ランタ ランタ
          く       タン



   ♪    Å
     ♪ / \   ランタ ランタ
      ヽ(;´Д`)ノ  ランタ タン
         (へ  )    ランタ タンタ
             >    タン

227 :132人目の素数さん:2022/05/02(月) 10:30:03 ID:DYgxe9pf.net
   | \
   |Д`) ダレモイナイ・・オドルナラ イマノウチ
   |⊂
   |


     ♪  Å
   ♪   / \   ランタ タン
      ヽ(´Д`;)ノ   ランタ タン
         (  へ)    ランタ ランタ
          く       タン



   ♪    Å
     ♪ / \   ランタ ランタ
      ヽ(;´Д`)ノ  ランタ タン
         (へ  )    ランタ タンタ
             >    タン

228 :132人目の素数さん:2022/12/21(水) 23:02:26.60 ID:F669Iarw.net
https://i.imgur.com/3dbELVo.jpg
https://i.imgur.com/KhOaFYh.jpg
https://i.imgur.com/G6EhYnQ.jpg
https://i.imgur.com/Wko98J0.jpg
https://i.imgur.com/lBK5S88.jpg
https://i.imgur.com/wiB134L.jpg
https://i.imgur.com/dfbPv74.jpg
https://i.imgur.com/JV7dvrw.jpg
https://i.imgur.com/5Xy5Ysa.jpg
https://i.imgur.com/gG6jyLz.jpg
https://i.imgur.com/ecuGrKr.jpg
https://i.imgur.com/hqUKYvN.jpg

229 :132人目の素数さん:2022/12/22(木) 04:01:55.01 ID:o2STx9rz.net
ゲーデルの不完全性定理の証明とか、

選択公理が命題として他の公理とは独立であることの証明とかできるかな?

もっと素朴に、√2が有理数では無いことの証明とか、
eやπが有理数ではないことの証明とか、
複素数係数の代数方程式は複素数の根を必ず持つことの証明とか。。。

230 :132人目の素数さん:2022/12/22(木) 08:30:52.51 ID:cem5kJiD.net
素数が無限個だったら Lean で見たなあ

231 :132人目の素数さん:2022/12/22(木) 08:49:17.37 ID:XxbM8r76.net
このようなソフトウェアに興味があるのですが、使えるようになるには、「証明論」のような本を
勉強しないとだめですよね。

232 :132人目の素数さん:2022/12/22(木) 09:04:01.71 ID:cem5kJiD.net
>>231
数学の知識よりも、プログラミングの知識のほうが重要だと思う。
関数型言語についてとか。

233 :132人目の素数さん:2022/12/22(木) 11:50:58.34 ID:5XpbsjKj.net
>>229
>ゲーデルの不完全性定理の証明
無矛盾(矛盾が証明されない)ならば
無矛盾性が証明されない、と読むから
神秘性や難しさを感じる

矛盾が証明されると矛盾する、という証明から
矛盾の証明が出来る、と読めばただのトリック

234 :132人目の素数さん:2022/12/22(木) 11:55:35.37 ID:5XpbsjKj.net
>>231
初心者は必ず騙されるが
証明論とは命題の証明方法の理論ではない

ちなみに命題の証明方法は別に難しくない
ただ証明がない場合、止まらないので
「アルゴリズム」とは言えないが

235 :132人目の素数さん:2022/12/22(木) 21:53:35.10 ID:cEUYFyKL.net
>>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 だけど

236 :132人目の素数さん:2022/12/22(木) 22:24:29.52 ID:qt1+aLga.net
>>232
数学とプログラミングが統一される前に時間切れでシンギュラリティが来そう。

237 :132人目の素数さん:2022/12/23(金) 21:32:30.54 ID:hmYygAkB.net
証明が存在する命題は、有限回の操作によって必ず証明にたどり着く方法はある。
ただし、その有限回なる回数が一体どのぐらいの有限なのかだ。宇宙が終わるまで
かけても終わらない程の大きな回数であっても有限だから。

238 :132人目の素数さん:2023/01/01(日) 23:05:56.42 ID:bVpk4vzc.net
ある命題の成立に対して正しい証明が得られたならば、
その証明が正しいことを確認する作業は、必ず証明の
記述の長さの多項式オーダーの手間で可能なのだろうか?

239 :132人目の素数さん:2023/01/01(日) 23:56:22.15 ID:A06C+pkU.net
証明が正しい事の証明、か

240 :132人目の素数さん:2023/01/02(月) 10:48:55.13 ID:Tjm8RrUz.net
(Coqのような)証明系は正しい証明を記述したならば、それが正しいことを
必ず有限の時間で検証を終えて停止するのだろうか?
その有限の時間だといっても途方も無く長くなったりしないのだろうか? 
検証を行う前に、証明の記述に応じてそれに対する検証時間の上界が
事前に得られるものだろうか?
それともそのような上界は一般にはなくて、ただただ結果が出るまで
ずーっと待って運良く生きているうちに終わることを期せねばならないのだろうか?

C言語とかAlgolのような普通のプログラミング言語は、
コンパイルすべきプログラムの長さNに対するコンパイル完了までの時間は
O(N log N)程度になってる。もしもコンパイルの時間がたとえばO(N^2)
かかるような言語とかコンパイラであると、プログラムの記述が大規模になれば
実用性が低くて使い物にならない感じになる。

241 :132人目の素数さん:2023/01/02(月) 11:14:46.62 ID:bB/h5A70.net
>>240
証明になっているか否かのチェックは有限時間で可能

証明になってないギャップについて
ギャップが埋められるかどうかは
命題が証明できるかどうかと同じなので
有限時間では判定できない

242 :132人目の素数さん:2023/01/02(月) 11:59:40.21 ID:Tjm8RrUz.net
「証明」の長さがNであるときに、検証にかかる計算量がNについてあまり急増化
しないのであれば、検証システムは使い物になるが、Nについてたとえば多項式
オーダーではなかったならば、少しばかり長い「証明」を検証しようとすれば
現実的には「いつまでたっても終わらないなぁsigh、修論が落ちるな」、
ということになりそうだけれども、そのあたりはどうなっているのでしょうか?

243 :132人目の素数さん:2023/01/02(月) 12:03:04.48 ID:Tjm8RrUz.net
検証系が進歩した未来において、

 著者は自分の証明を検証系にかけて、
検証系に与えたソースコードも併せて提出する。
 論文の査読者はそのソースコードが正しく論文の定理や命題を表していることを
(ああたいへんだ)チェックして(そこが間違ってたらどうする?)、
検証系にかけて、正しく証明されることを確認したら、アクセプトする。

そうなったらとても面倒。論文のLaTeXのソースを提出するのとは次元が違う。

244 :132人目の素数さん:2023/01/03(火) 02:56:16.38 ID:EWDc62a3.net
ABC予想の証明の検証に時間がかかっていたようだけど、
Coqで検証すればよかったんじゃないの?できないの?

245 :132人目の素数さん:2023/01/03(火) 04:56:18.54 ID:JnLpt9Qh.net
人間の書いた人間に理解できるように書かれた証明を、
いろいろな前提知識の無い無垢のソフトに全く隙のない形で
完璧に記号だけを使って記述し直すというのは、とても大変な
作業になるだろう。暗黙知、専門家の常識、そういうものを総動員して
それらも含めて検証にかけなければ、論理が飛んでいることになるから
だろう。

246 :132人目の素数さん:2023/01/03(火) 13:33:16.33 ID:EWDc62a3.net
ABC予想の証明に否定的な数学者もいるようですから、
白黒はっきりつけるためにはした方が良さそうですね
おそろしく時間とお金(人件費)が掛かりそうですが…

247 :132人目の素数さん:2023/01/03(火) 13:35:59.35 ID:EWDc62a3.net
今まで正しいと思われていた定理がCoqで検証をしたら証明が間違っていて実は成立していなかった
という場合はあり得るのだろうか?

248 :132人目の素数さん:2023/01/03(火) 21:49:08.81 ID:JnLpt9Qh.net
定理をみな洗濯して候。選択公理を密輸入してたりとか。

249 :132人目の素数さん:2023/01/05(木) 07:12:53.60 ID:YJDwUIlt.net
基本的な質問で申し訳ありませんが、任意の数学の定理の証明は
その証明が正しいならばコンピューターが理解できる形の形式的な証明に書き直せますよね?

250 :132人目の素数さん:2023/01/05(木) 09:40:00.61 ID:9UuOCWgb.net
>>249
非構成的な証明とかは、形式的な証明に落とし込めるのかなあ?

251 :132人目の素数さん:2023/01/06(金) 11:00:40.85 ID:YgDL6YiZ.net
数学によってはインフォーマルな証明ってのがあるかも

252 :132人目の素数さん:2023/01/11(水) 00:03:59.83 ID:NoXe1rzD.net
数学を外から眺めているメタ数学、そのメタ数学を外から眺めているメタメタ数学、
そのメタメタ数学を外から眺めているメタメタメタ数学、とどこまでいっても
その外側から眺めている数学があるのだとしたら。この宇宙も、メタ宇宙の中で
眺められ観察され実験されている存在なのじゃないかと思えてくる。
ある日、これじゃダメだな、やり直すかという声が聞こえてきて。。。

253 :132人目の素数さん:2023/01/12(木) 23:28:57.14 ID:AOFqi22d.net
形式化されていない証明は人間(数学者)が検証したものに過ぎないから
証明が正しい可能性が極めて高い、としか言えなくて
厳密に正しいとは確定していないように思うがどうだろう

254 :132人目の素数さん:2023/01/12(木) 23:41:41.72 ID:AKp/tV8W.net
厳密というのは程度の問題だからね

255 :132人目の素数さん:2023/01/13(金) 09:24:12.80 ID:22h15Q8H.net
線型偏微分方程式の解が存在しない例
smooth linear partial differential equation without solution
https://planetmath.org/smoothlinearpartialdifferentialequationwithoutsolution

解が存在しないことを証明できますか?

256 :132人目の素数さん:2023/01/13(金) 18:19:38.43 ID:22h15Q8H.net
できないわけね、了解

257 :132人目の素数さん:2023/01/13(金) 19:43:33.22 ID:C3eRYlyK.net
ある命題の証明が存在しないものと仮定して、
それから矛盾を出してやり、よって証明は存在する。
しかし具体的に証明を構成しない。

そういうやり方の「証明」はCoqで記述できるのかな?

258 :132人目の素数さん:2023/01/14(土) 01:43:50.64 ID:qnmCJki9.net
ちょっとググってみて >>257さん とはずれるかもだけど、こんな記事を見つけた。
ゲーデル数化とかガチで出来るんだね。すごいわ。

ゲーデルの不完全性定理の形式証明を読む
https://qiita.com/41semicolon/items/caceb8bc52172190902d

259 :132人目の素数さん:2023/01/15(日) 21:23:10.70 ID:iLTqkcdp.net
>>257
背理法を使わずに対偶で書き直せばできるのでは?

260 :132人目の素数さん:2023/01/27(金) 02:52:52.56 ID:iXvRI0Bd.net
"クルト・ゲーデル 史上最もスキャンダラスな定理を証明した男", 森北出版, 2023年2月.

261 :132人目の素数さん:2023/01/28(土) 09:08:50.72 ID:YuG7Qllk.net
>>258
>ゲーデル数化とかガチで出来るんだね。すごいわ。
 コード化は別に難しくない
 証明可能性述語の記述のほうが面倒
 まあでもやればできるだろうな
 別に神秘的なことはやってない

262 :132人目の素数さん:2023/01/28(土) 09:21:22.14 ID:YuG7Qllk.net
>>260
>”クルト・ゲーデル 史上最もスキャンダラスな定理を証明した男”
 タイトルが大袈裟すぎw

 原題は"Journey to the Edge of Reason"
 著者のStephen Budianskyは、別に数学者ではないらしい
 
 ゲーデルの生涯に関心があるなら
 Dawsonの"Logical Dilemma"を読むことを勧める
 日本語訳もある

 不完全性定理について知りたいなら
 ホフスタッターのゲーデル・エッシャ―・バッハの
 第14章を読んだほうがいい

 興味深い定理であることは確かだが
 なんか持ち上げられすぎ
 ゲーデル自身は理性の完全性を信じていたので
 不完全性定理の結論は彼の願望とは必ずしも合致しない

263 :132人目の素数さん:2023/01/28(土) 10:20:43.69 ID:k/vPDvzu.net
【キッシンジャー】 ワクチンを強制し群れを減らす
://rio2016.5ch.net/test/read.cgi/lifesaloon/1662167492/l50
https://o.5ch.net/1ztpf.png

264 :132人目の素数さん:2023/01/29(日) 17:51:01.73 ID:wni79iFl.net
帝銀事件とは

戦後まだGHQが日本を占領していた頃のことである。
都内は椎名町にあった帝国銀行に白衣を着た男がやって来て
保健所から来た。近所で赤痢(?)が発生した。だがこの
薬をのめば感染を防げると行内の客や行員に言って、
薬の飲み方を実演して見せて、そうして一人ずつ呑ませて
いった。呑んですぐには症状が出なかったので、みんな
おとなしく従って呑んだが、しばらくすると次々と倒れて、
その男は行内から手形だったか僅かな金を持って逃げた。
という事件だ。

これを今のコロナ騒動・ワクチンの話に照らして考えてみると
面白い。

遅効性の薬物(即座に効果が出ずに、ある程度時間が経ってから
効果を発揮する)は、それが毒作用を持つものであれば、後で
大量の薬害を生みかねない。日本向けに特別にカスタマズされた
ものだったりすると、日本民族全滅も可能。

265 :132人目の素数さん:2023/02/10(金) 01:08:15.66 ID:Gw+Md1wQ.net
日本マイクロソフトと東京都、DX推進に向けた協定を締結
https://pc.watch.impress.co.jp/docs/news/1477452.html

行政とIT企業との関係。住民の情報をどこかに

266 :132人目の素数さん:2023/02/14(火) 01:02:00.55 ID:5OXageYe.net
Coqのシステムが書かれているソースコードを形式化して、
Coqに証明させようとすると、どうなるだろうか?
そういうことを考えると、脳外科が自分で自分の脳の手術
をするというような、なんだかとてもいやーぁな感じがする。

267 :132人目の素数さん:2023/02/14(火) 02:10:03.23 ID:One+2Hab.net
不動点意味論

268 :132人目の素数さん:2023/02/14(火) 12:13:54.45 ID:5OXageYe.net
Coqの検証系がCoqの形式記述に証明不可能な部分を見つけたと主張した場合に、
その部分の影響でCoqの検証系が正しく動作しないためであるのかどうかが
怪しくなる。
ソースコードから形式記述を作り出すところの正しさも証明しなければならない
はずだし。その形式記述を作り出すシステムの正しさも証明しなければならないが、
。。。。とやっていると、本当の正しさを証明するということは、無理じゃね?
という暗澹たる気持ちになる。結局は正しさというのは信仰の一種であるか、
何かを信じることで魂の安らかさを得る必要があり、心に不安があると
Gのようにキチガイになったりすると思う。

269 :132人目の素数さん:2023/02/23(木) 20:40:51.53 ID:6O/Q2IOx.net
Gって何?

270 :132人目の素数さん:2023/03/04(土) 14:12:35.38 ID:qLJkywT3.net
論理のよりどころは最後は神の存在に行き着くのだろう。
そうして論理は言葉(記号)によって書かれる。

現代の数学はユダヤ教の思考の派生品なのかもしれない。

271 :132人目の素数さん:2023/03/16(木) 17:45:06.78 ID:/qOR2FZK.net
質問です

下記のcase tacticでなぜ証明終わるでしょうか?
場合分けのためと理解しているので、なぜ終わるかわかりません。

Lemma f_test :forall A:Prop, A -> not A -> True.
Proof.
intros H H0 H1.
case (H1 H0).
Qed.

272 :132人目の素数さん:2023/03/16(木) 19:54:34.57 ID:v6yT4YhJ.net
>>271

https://magicant.github.io/programmingmemo/coq/byhyp.html
ここに「前提が False の場合」の説明が載っている。

以下だと分かりやすいかも
Lemma f_test :forall A:Prop, A -> not A -> True.
Proof.
intros H H0 H1.
apply H1 in H0.
case H0.
Qed.

273 :132人目の素数さん:2023/03/16(木) 22:10:00.35 ID:/qOR2FZK.net
>>272

ありがとうございます。わかりました。

caseの対象がFalseになっていて、
コンストラクタがないため終了と。

274 :132人目の素数さん:2023/03/17(金) 20:00:33.56 ID:3R+VYxhu.net
哀れGは神の存在を証明するなどと言いだして周囲は彼を  扱いしたという。

275 :132人目の素数さん:2023/07/29(土) 03:40:44.18 ID:fNEHywFwq
海外の環境団体はあらゆる妨害活動から破壞活動までやってて人としての最低限の道徳を知ってて素晴らしいか゛曰本にはクス゛しかいないのかよ
せめて広島の平和公園もとい地球破壞公園の殺人の灯でВвQくらいやってみせろや.何しろ肉を焼くわけて゛もなく、月に8О0立方メ─├ル
ものプ□パンカ゛スをたた゛ひたすら燃やし続けていやか゛るんた゛からな,せめて肉て゛も焼いてみせて気侯変動に抗議する象徴的行動するのか゛人の道
莫大な温室効果ガスまき散らして世界ー周旅行して、サミットた゛のと國民から強奪した莫大な税金無駄にしながら飲み食い観光.警備た゛のと
クソシナ顔負けの私権侵害やって世界中にハ゛力晒し続けてる岸田異次元増税憲法ガン無視地球破壞軍国主義売国奴文雄みたいなクズた゛の、
持続可能な開発目標に壞滅的なダメ−ジを及ぼすために國連本部にノコ丿コ出かけて莫大な温室効果カ゛スまき散らす広島県知事湯崎英彦だのを
当選させてる広島県民は恥を知れよ、広島原爆て゛14万人殺されたそうだか゛.Wм〇が確認したた゛けで197○年以降に氣侯変動によって、
土砂崩れに洪水,暴風.猛暑.大雪やら災害で殺された人数は2〇О萬人以上、経済損失は6Ο○兆圓以上という現実を理解しろタ゛フ゛ス夕県民

創価学会員は.何百萬人も殺傷して損害を与えて私腹を肥やし続けて逮捕者まで出てる世界最惡の殺人腐敗組織公明党を
池田センセ─か゛囗をきけて容認するとか本気て゛思ってるとしたら侮辱にもほと゛か゛あるそ゛!
hтТрs://i、imgur.сom/hnli1ga.jpeg

総レス数 275
75 KB
掲示板に戻る 全部 前100 次100 最新50
read.cgi ver 2014.07.20.01.SC 2014/07/20 D ★