【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

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

**１３２人目の素数さん** · 2023/01/05(木) 09:40:00.61

>>249
非構成的な証明とかは、形式的な証明に落とし込めるのかなあ？

**１３２人目の素数さん** · 2023/01/06(金) 11:00:40.85

数学によってはインフォーマルな証明ってのがあるかも

**１３２人目の素数さん** · 2023/01/11(水) 00:03:59.83

数学を外から眺めているメタ数学、そのメタ数学を外から眺めているメタメタ数学、
そのメタメタ数学を外から眺めているメタメタメタ数学、とどこまでいっても
その外側から眺めている数学があるのだとしたら。この宇宙も、メタ宇宙の中で
眺められ観察され実験されている存在なのじゃないかと思えてくる。
ある日、これじゃダメだな、やり直すかという声が聞こえてきて。。。

**１３２人目の素数さん** · 2023/01/12(木) 23:28:57.14

形式化されていない証明は人間（数学者）が検証したものに過ぎないから
証明が正しい可能性が極めて高い、としか言えなくて
厳密に正しいとは確定していないように思うがどうだろう

**１３２人目の素数さん** · 2023/01/12(木) 23:41:41.72

厳密というのは程度の問題だからね

**１３２人目の素数さん** · 2023/01/13(金) 09:24:12.80

線型偏微分方程式の解が存在しない例
smooth linear partial differential equation without solution
https://planetmath.org/smoothlinearpartialdifferentialequationwithoutsolution

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

**１３２人目の素数さん** · 2023/01/13(金) 18:19:38.43

できないわけね、了解

**１３２人目の素数さん** · 2023/01/13(金) 19:43:33.22

ある命題の証明が存在しないものと仮定して、
それから矛盾を出してやり、よって証明は存在する。
しかし具体的に証明を構成しない。

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

**１３２人目の素数さん** · 2023/01/14(土) 01:43:50.64

ちょっとググってみて >>257さんとはずれるかもだけど、こんな記事を見つけた。
ゲーデル数化とかガチで出来るんだね。すごいわ。

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

**１３２人目の素数さん** · 2023/01/15(日) 21:23:10.70

>>257
背理法を使わずに対偶で書き直せばできるのでは？

**１３２人目の素数さん** · 2023/01/27(金) 02:52:52.56

"クルト・ゲーデル史上最もスキャンダラスな定理を証明した男", 森北出版, 2023年2月.

**１３２人目の素数さん** · 2023/01/28(土) 09:08:50.72

>>258
>ゲーデル数化とかガチで出来るんだね。すごいわ。
　コード化は別に難しくない
　証明可能性述語の記述のほうが面倒
　まあでもやればできるだろうな
　別に神秘的なことはやってない

**１３２人目の素数さん** · 2023/01/28(土) 09:21:22.14

>>260
>”クルト・ゲーデル史上最もスキャンダラスな定理を証明した男”
　タイトルが大袈裟すぎｗ

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

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

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

**１３２人目の素数さん** · 2023/01/28(土) 10:20:43.69

【キッシンジャー】　ワクチンを強制し群れを減らす
://rio2016.5ch.net/test/read.cgi/lifesaloon/1662167492/l50

**１３２人目の素数さん** · 2023/01/29(日) 17:51:01.73

帝銀事件とは

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

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

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

**１３２人目の素数さん** · 2023/02/10(金) 01:08:15.66

日本マイクロソフトと東京都、DX推進に向けた協定を締結
https://pc.watch.impress.co.jp/docs/news/1477452.html

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

**１３２人目の素数さん** · 2023/02/14(火) 01:02:00.55

Coqのシステムが書かれているソースコードを形式化して、
Coqに証明させようとすると、どうなるだろうか？
そういうことを考えると、脳外科が自分で自分の脳の手術
をするというような、なんだかとてもいやーぁな感じがする。

**１３２人目の素数さん** · 2023/02/14(火) 02:10:03.23

不動点意味論

**１３２人目の素数さん** · 2023/02/14(火) 12:13:54.45

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

**１３２人目の素数さん** · 2023/02/23(木) 20:40:51.53

Gって何？

**１３２人目の素数さん** · 2023/03/04(土) 14:12:35.38

論理のよりどころは最後は神の存在に行き着くのだろう。
そうして論理は言葉（記号）によって書かれる。

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

**１３２人目の素数さん** · 2023/03/16(木) 17:45:06.78

質問です

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

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

**１３２人目の素数さん** · 2023/03/16(木) 19:54:34.57

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

**１３２人目の素数さん** · 2023/03/16(木) 22:10:00.35

>>272

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

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

**１３２人目の素数さん** · 2023/03/17(金) 20:00:33.56

哀れGは神の存在を証明するなどと言いだして周囲は彼を　　扱いしたという。