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

**１３２人目の素数さん** · 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

数学者の定義しだい

**１３２人目の素数さん** · 2020/02/24(月) 04:56:39.43

>>7
> English speakerに前置きなく「コック」って言ったら誤解を産むよね
日本語話者にも開発者のCoquandの名前を「コカン」って呼んだら誤解生みそう

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

？？？？？

**１３２人目の素数さん** · 2020/03/13(金) 02:15:49.03

Coqのライブラリ集ってどう探しますか？

**１３２人目の素数さん** · 2020/04/08(水) 03:27:53.06

ggl

**１３２人目の素数さん** · 2020/04/28(火) 21:44:58.39

数学の教科書をcoqで翻訳して公開したら著作権違反になりますか？

**１３２人目の素数さん** · 2020/08/31(月) 18:29:37.56

これでMathematicaみたいなことができるの？

**１３２人目の素数さん** · 2020/08/31(月) 19:38:58.46

>>207
それは翻訳じゃなくて詳細な機械証明をつけたことになるからいいんじゃね？

やれるもんならやってごらん（挑発）

**１３２人目の素数さん** · 2020/09/01(火) 19:16:57.55

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

**１３２人目の素数さん** · 2020/12/29(火) 17:55:55.21

>>209
ありがとうございます😊
やってみようと思います。

**１３２人目の素数さん** · 2020/12/29(火) 18:10:40.92

Coqとかのソフトウェアを理解して使えるようになるには，どんな本を読めばいいですか？

**１３２人目の素数さん** · 2020/12/29(火) 19:37:12.97

本なら『Coq/SSReflect/MathCompによる定理証明』かな。実際に使って証明したいものを証明した方が良いと思うけど。

**１３２人目の素数さん** · 2020/12/29(火) 20:13:39.22

>>213
ありがとうございます．
その本は読んだことがあるのですが，何が書いてあるのかよくわかりませんでした．
その本を読むための予備知識はどんな本を読めばいいのでしょうか？

**１３２人目の素数さん** · 2020/12/29(火) 22:12:44.60

Coqで何をしたいのかは分からないけど、数学の証明をしたいのなら命題論理とか述語論理の勉強をしたらいいと思うよ。

**１３２人目の素数さん** · 2020/12/30(水) 05:46:12.85

プログラムの観点から言うと、「依存型」「カリー＝ハワード同型対応」がキーワードになるかな。
あんまり伸びてないけど、ム板にこういうスレがある。

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

**１３２人目の素数さん** · 2021/03/04(木) 23:54:49.26

F x = If x < 10 then x else F (x - 1)

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

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

**１３２人目の素数さん** · 2021/03/05(金) 08:47:36.61

>>217
はっきり見てないけど、こことか参考にならないかな？
https://stackoverflow.com/questions/16555022/proving-if-then-else-in-coq

**１３２人目の素数さん** · 2021/03/05(金) 09:33:07.21

>>218
まさにこれっぽいです。ありがとうございます！

**１３２人目の素数さん** · 2021/04/18(日) 19:19:36.97

Coqで日本語データを処理するプログラム書けますか？
Asciiは扱えるみたいです。

**１３２人目の素数さん** · 2021/06/13(日) 11:30:42.81

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

**１３２人目の素数さん** · 2021/06/13(日) 12:05:53.03

>>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) の部分の括弧は外す事ができる。

**１３２人目の素数さん** · 2021/06/17(木) 19:16:48.45

証明支援システムCoq、新しい名称を検討中
https://developers.srad.jp/story/21/06/16/1737205/

**１３２人目の素数さん** · 2022/01/12(水) 08:10:41.00

コックむずい

**１３２人目の素数さん** · 2022/01/24(月) 07:16:51.96

ムズいよねえ
もっと勉強しなくては

**１３２人目の素数さん** · 2022/02/11(金) 01:30:20.50

　　　| ＼
　　　|Д｀)　ﾀﾞﾚﾓｲﾅｲ･･ｵﾄﾞﾙﾅﾗｲﾏﾉｳﾁ
　　　|⊂
　　　|

　　　　　♪　　Å
　　　♪　　　／＼　　　ﾗﾝﾀﾀﾝ
　　　　　　ヽ(´Д｀;)ﾉ　　ﾗﾝﾀﾀﾝ
　　　　　　 (　へ) 　　　ﾗﾝﾀﾗﾝﾀ
　　　　　　く　　　　　　ﾀﾝ

　　　♪　　　　Å
　　　　　♪　／＼　　　ﾗﾝﾀﾗﾝﾀ
　　　　　　ヽ（;´Д｀）ﾉ　　ﾗﾝﾀﾀﾝ
　　　　　　 (へ　 ) 　　　ﾗﾝﾀﾀﾝﾀ
　　　　　　　　 >　　　　ﾀﾝ

**１３２人目の素数さん** · 2022/05/02(月) 10:30:03.66

　　　| ＼
　　　|Д｀)　ﾀﾞﾚﾓｲﾅｲ･･ｵﾄﾞﾙﾅﾗｲﾏﾉｳﾁ
　　　|⊂
　　　|

　　　　　♪　　Å
　　　♪　　　／＼　　　ﾗﾝﾀﾀﾝ
　　　　　　ヽ(´Д｀;)ﾉ　　ﾗﾝﾀﾀﾝ
　　　　　　 (　へ) 　　　ﾗﾝﾀﾗﾝﾀ
　　　　　　く　　　　　　ﾀﾝ

　　　♪　　　　Å
　　　　　♪　／＼　　　ﾗﾝﾀﾗﾝﾀ
　　　　　　ヽ（;´Д｀）ﾉ　　ﾗﾝﾀﾀﾝ
　　　　　　 (へ　 ) 　　　ﾗﾝﾀﾀﾝﾀ
　　　　　　　　 >　　　　ﾀﾝ

**１３２人目の素数さん** · 2022/12/21(水) 23:02:26.60

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

**１３２人目の素数さん** · 2022/12/22(木) 04:01:55.01

ゲーデルの不完全性定理の証明とか、

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

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

**１３２人目の素数さん** · 2022/12/22(木) 08:30:52.51

素数が無限個だったら Lean で見たなあ

**１３２人目の素数さん** · 2022/12/22(木) 08:49:17.37

このようなソフトウェアに興味があるのですが、使えるようになるには、「証明論」のような本を
勉強しないとだめですよね。

**１３２人目の素数さん** · 2022/12/22(木) 09:04:01.71

>>231
数学の知識よりも、プログラミングの知識のほうが重要だと思う。
関数型言語についてとか。

**１３２人目の素数さん** · 2022/12/22(木) 11:50:58.34

>>229
>ゲーデルの不完全性定理の証明
無矛盾(矛盾が証明されない)ならば
無矛盾性が証明されない、と読むから
神秘性や難しさを感じる

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

**１３２人目の素数さん** · 2022/12/22(木) 11:55:35.37

>>231
初心者は必ず騙されるが
証明論とは命題の証明方法の理論ではない

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

**１３２人目の素数さん** · 2022/12/22(木) 21:53:35.10

>>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 だけど

**１３２人目の素数さん** · 2022/12/22(木) 22:24:29.52

>>232
数学とプログラミングが統一される前に時間切れでシンギュラリティが来そう。

**１３２人目の素数さん** · 2022/12/23(金) 21:32:30.54

証明が存在する命題は、有限回の操作によって必ず証明にたどり着く方法はある。
ただし、その有限回なる回数が一体どのぐらいの有限なのかだ。宇宙が終わるまで
かけても終わらない程の大きな回数であっても有限だから。

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

ある命題の成立に対して正しい証明が得られたならば、
その証明が正しいことを確認する作業は、必ず証明の
記述の長さの多項式オーダーの手間で可能なのだろうか？

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

証明が正しい事の証明、か

**１３２人目の素数さん** · 2023/01/02(月) 10:48:55.13

（Coqのような）証明系は正しい証明を記述したならば、それが正しいことを
必ず有限の時間で検証を終えて停止するのだろうか？
その有限の時間だといっても途方も無く長くなったりしないのだろうか？　
検証を行う前に、証明の記述に応じてそれに対する検証時間の上界が
事前に得られるものだろうか？
それともそのような上界は一般にはなくて、ただただ結果が出るまで
ずーっと待って運良く生きているうちに終わることを期せねばならないのだろうか？

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

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

>>240
証明になっているか否かのチェックは有限時間で可能

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

**１３２人目の素数さん** · 2023/01/02(月) 11:59:40.21

「証明」の長さがNであるときに、検証にかかる計算量がNについてあまり急増化
しないのであれば、検証システムは使い物になるが、Nについてたとえば多項式
オーダーではなかったならば、少しばかり長い「証明」を検証しようとすれば
現実的には「いつまでたっても終わらないなぁsigh、修論が落ちるな」、
ということになりそうだけれども、そのあたりはどうなっているのでしょうか？

**１３２人目の素数さん** · 2023/01/02(月) 12:03:04.48

検証系が進歩した未来において、

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

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

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

ABC予想の証明の検証に時間がかかっていたようだけど、
Coqで検証すればよかったんじゃないの？できないの？

**１３２人目の素数さん** · 2023/01/03(火) 04:56:18.54

人間の書いた人間に理解できるように書かれた証明を、
いろいろな前提知識の無い無垢のソフトに全く隙のない形で
完璧に記号だけを使って記述し直すというのは、とても大変な
作業になるだろう。暗黙知、専門家の常識、そういうものを総動員して
それらも含めて検証にかけなければ、論理が飛んでいることになるから
だろう。

**１３２人目の素数さん** · 2023/01/03(火) 13:33:16.33

ABC予想の証明に否定的な数学者もいるようですから、
白黒はっきりつけるためにはした方が良さそうですね
おそろしく時間とお金（人件費）が掛かりそうですが…

**１３２人目の素数さん** · 2023/01/03(火) 13:35:59.35

今まで正しいと思われていた定理がCoqで検証をしたら証明が間違っていて実は成立していなかった
という場合はあり得るのだろうか？

**１３２人目の素数さん** · 2023/01/03(火) 21:49:08.81

定理をみな洗濯して候。選択公理を密輸入してたりとか。

**１３２人目の素数さん** · 2023/01/05(木) 07:12:53.60

基本的な質問で申し訳ありませんが、任意の数学の定理の証明は
その証明が正しいならばコンピューターが理解できる形の形式的な証明に書き直せますよね？

**１３２人目の素数さん** · 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は神の存在を証明するなどと言いだして周囲は彼を　　扱いしたという。