Coqスレ

こけこっこー
http://coq.inria.fr/

興味はあるが……

Ｃｏｑ！Ｃｏｑ！Ｃｏｑ！Ｃｏｑぅぅうううわぁああああああああああああああああああああああん！！！
あぁああああ…ああ…あっあっー！あぁああああああ！！！ＣｏｑＣｏｑＣｏｑぅううぁわぁああああ！！！
あぁクンカクンカ！クンカクンカ！スーハースーハー！スーハースーハー！いい匂いだなぁ…くんくん
んはぁっ！ＰｒｏｏｆＧｅｎｅｒａｌたんの桃色ブロンドの髪をクンカクンカしたいお！クンカクンカ！あぁあ！！
間違えた！モフモフしたいお！モフモフ！モフモフ！髪髪モフモフ！カリカリモフモフ…きゅんきゅんきゅい！！
小説11巻のＣｏｑたんかわいかったよぅ！！あぁぁああ…あああ…あっあぁああああ！！ふぁぁあああんんっ！！
アニメ2期決まって良かったねＣｏｑたん！あぁあああああ！かわいい！Ｃｏｑたん！かわいい！あっああぁああ！
コミック2巻も発売されて嬉し…いやぁああああああ！！！にゃああああああああん！！ぎゃああああああああ！！
ぐあああああああああああ！！！コミックなんて現実じゃない！！！！あ…小説もアニメもよく考えたら…
Ｃ ｏ ｑ ち ゃ ん は 現実的 じ ゃ な い？にゃあああああああああああああん！！うぁああああああああああ！！
そんなぁああああああ！！いやぁぁぁあああああああああ！！はぁああああああん！！Ｒｏｃｑｕｅｎｃｏｕｒｔぅああああ！！
この！ちきしょー！やめてやる！！現実なんかやめ…て…え！？見…てる？ターミナルのＣｏｑちゃんが僕を見てる？
ターミナルのＣｏｑちゃんが僕を見てるぞ！Ｃｏｑちゃんが僕を見てるぞ！バッファのＣｏｑちゃんが僕を見てるぞ！！
アニメのＣｏｑちゃんが僕に話しかけてるぞ！！！よかった…世の中まだまだ捨てたモンじゃないんだねっ！
いやっほぉおおおおおおお！！！僕にはＣｏｑちゃんがいる！！やったよケティ！！ひとりでできるもん！！！
あ、コミックのＣｏｑちゃああああああああああああああん！！いやぁあああああああああああああああ！！！！
あっあんああっああんあアン様ぁあ！！セ、セイバー！！シャナぁああああああ！！！ヴィルヘルミナぁあああ！！
ううっうぅうう！！俺の想いよＣｏｑへ届け！！ＩＮＲＩＡのＣｏｑへ届け！

このスレッドは天才チンパンジー「アイちゃん」が
言語訓練のために立てたものです。

アイと研究員とのやり取りに利用するスレッドなので、
関係者以外は書きこまないで下さい。

　　　　　　　　　　　　　　　　　　京都大学霊長類研究所

Gaaaaaaaaaaaaaze at my biiiiiiiiiiiig coooooooq!

これ日本にいるユーザ数ってどれくらいなの？

まともなレスがつかないから、だれか紹介サイトとかテンプレとか作ったらどう?
興味をそそるような紹介文とか書かないと、ほとんどの人は食いついてこないよ。

>>7
食いついたって仕方の無い言語

そうでもないよ

Coq は、INRIA にて開発されている対話的定理証明支援系です。 Calculus of Inductive Construction (CIC) を基礎とし、Tactics と呼ばれるコマンドを駆使することにより証明を行います。

http://www.eva-01.jp/wiki/pukiwiki.php?Coq

証明のゴルフ場があったぞ。ダレとくwww

http://d.hatena.ne.jp/kikx/20100807

女子高生によるほんわかCoqチュートリアルキター！！！！
むねあつ！!!
http://www.iij-ii.co.jp/lab/techdoc/coqt/

＊ 「Coq！Coq！Coq！ どいつもこいつもCoq！
　　なぜだ！　なぜやつを認めて　このおれを認めねえんだ！」

>>13
誰だお前？

>>13
Isabelle乙

>>15
実はAgdaじゃね？
こっちも依存型なのにCoqよりマイナーなのが悔しいとか。

>>16
Agdaの機能やシンタックスはかなりCoqにも影響を与えているよね。
id: forall {A: Type}, A -> A の{}とか。
国産の定理証明器だからぜひともがんばってほしいものだが。

>>17
確かに日本の人も貢献してるけど、北欧モノだよね？

Goal False <> True.

>>12
2章が公開されたね。
問5がわからない……

問5は apply (H (or P (~P))). がヒントかな

>>19
intro.

>>19
intro H.
symmetry in H.
induction H.
auto.

>>22
rewrite H.

>>12
読み始めたけど、素人っぽさはすごくあるな

初っぱなの"Definition"のDが大文字でなければならないことに注意が無かったり、
"Eval compute in"はプルダウンボックスから選ぶにもかかわらず、「左側のテキストボックスに……と打ち、」とか書いてあったり。
plus'やid'のアポストロフィが何の説明もなく出てきたり。

>>25
確かに説明はちょっと素人っぽいな。
しかし、少なくともCoqの知識はすごいな。高校生でCoqできるってなんか別の意味で人生楽しそうでいいな。
大人になったらなんの仕事をするんだろうか？

さては料理人だな

>>26
高校三年でCoqについて書けるのがすごいと思う。
フリーソフトの大部分は、高校レベルでは何するソフトかも想像できないのが普通だから。

将来は大学教授かテクニカルライターかな？
初学者の引っかかりやすい部分に注意を払えるようになって一人前なんだろうと思う。

大学で着実に勉強を重ねていって欲しいね。

俺も高校の時から英語の文献読んでたよ。
Coqは日本語の資料もあるし、それほど厳しくないと思われ

>>29
> Coqは日本語の資料もあるし、それほど厳しくないと思われ

どれのことですか？
教えてプリーズ。

自分は、高校数学の範囲は大人が思い出すよりかなり狭いと思うけどね。
述語論理、微分方程式の数値解法、品質管理に使う統計解析など、どれも高校数学には含まれない。

Coqで証明たてるのって、結構大変なんじゃないの？そこそこの経験者らしいよ。
相対論から量子コンピューターまでの英論文は、高校時代読むだけなら自分もやってたけど、使いこなしたことはない。

英語よりも、数学の基礎知識が不足するんじゃないかと思うのだけど。

>>31
> 相対論から量子コンピューターまでの英論文は、高校時代読むだけなら自分もやってたけど、使いこなしたことはない。

高校時代に偏微分方程式とか状態ベクトルとか推移行列とかヒルベルト空間とか？

内部進学者する人なら、高校時代に割と好きなこと勉強できるのかな？

与えられたものを必死で勉強する人間と、
自分で楽しい物を探して勉強する人間の違い。
優劣ではなく、ただの違い。

let と let recが違うのはカテゴリカルな意味が違うからだったはず。
CAMLってCategorical Abstract Machine Languageの略だし。
ソースは無い。

ML誤爆っすにゃ？

>>34
letrecの双対があるってこと？ほんまかいな。

双対？意味が違うから分けているんじゃないか、と言ってるだけだぞ。
スレチすまそ。

圏論でいう圏も哲学で使われる範疇も
どっちも英語としてはcategoryなんだよなややこしい

少なくともこのスレの文脈では全くややこしいことはなかった。

>>12
弱った。
チンプンカンプンだ。

説明が簡潔に過ぎる、ウルマンのMLの教科書などと比べて。

スタンフォード大学の偏差値の高い学生に教えるときですら、
ウルマンくらいの易しさが必要なのになあ。

自己紹介上手だね

山本和彦氏の指導の元で書かれたという前提で、さらに偏見を漏らしてみる。

山本和彦氏は自分がEngineerだと思っているようだ。
Educatorの発想が少し足りないのかもしれない。

Engineerは動くブラックボックスを作っていれば、
説明がテキトーでもバカにされることはない。

逆に、Educatorは理解できる説明をしなければならない。
ブラックボックスを作るとバカと呼ばれる。

アルバイトとかで、会社として管理職がいるだけじゃね？
本人は何やるかだけ承諾もらって、自由にやってるんだろう。
coqに興味あるなら、文章覚えるんじゃなくて、手を動かして覚えましょう。

教科書ほしいっていうのなら、
勉強会で使ってるのあるみたいだよ。
Certified Programming with Dependent Types
http://adam.chlipala.net/cpdt/html/toc.html
http://adam.chlipala.net/cpdt/cpdt.pdf

上階層貼ったほうがよかったね。ゴメン
http://adam.chlipala.net/cpdt/

>>44-45
ありがとう
とても面白そうだね
MIT Pressから本としてももうすぐ出版されるみたいだね
最近、この手の分野の本の出版がほとんどなかったから楽しみ
ひところはGunterとかWinskelとかMitchellとかBruceとかどんどん出たのに
やっぱり本の形の方がディスプレイよりも目も疲れなくて読みやすいから
本が出たら買うことにしよう

>>44
英語は苦手ですが、ありがとうございます。
いろいろな試行をやってみるところまで、何とかたどり着きたいです。

こんなところでformal semanticsの専門家にでくわすとは

Gunterいいよね。

>>48

うん、Gunterのはとても良い本だよね

Gunterってなんぞ？CPDTと関係あるのか？

Winskel の方が整理されてて良い、という人も多いが、
あれの良さがわからん。英語も変だし。

にわかだからYvesPierr、mathewぐらいしかわからん

>>52
> にわかだからYvesPierr、mathewぐらいしかわからん

さらにニワカなんで質問するんだけど、この２人ってどんな仕事してる人？
ググったけどわからない。

yvesはCoq'Artの著者の一人
matthieuは最近Coqに追加された機能Type Class, User defined　equialities and relations, Program等の中心開発者

>>54
ありがとうございました。
52に"YvesPierr、mathew"って書いてるから "Yves Pierre"が一人の名前だと思ってググったんだけど
でもYvesとPierreは別々の２人それぞれのファーストネームということなんですね。
それじゃググってもわからなくて当たり前でした。

正直、この歳になって女子大生の夏休みを心待ちにすることになるとは思わんかった

>>50
> Gunterってなんぞ？CPDTと関係あるのか？

49を書いて久しく見てなかったんですまない、質問が出てたんだね

Gunterというのは次の本のことです
Carl A. Gunter "Semantics of Programming Languages" (MIT Press, 1992)

この本はプログラミング言語に対する表示的意味論の本なんだが
それに必要な領域理論（domain theory: cpoとかの構成法やその圏論的な定式化とか）を市販の教科書の中では一番詳しく書いてある
（その方面専門の数学の専門書ならもっと詳しいのはいくらでもあるが計算機屋向けだとこれが一番詳しい）

共立の朱色のシリーズから出ていた横内さんの『プログラム意味論』（もう品切れ放置プレーされてるのかな、それともまだ出てるか？）は
ある意味ではGunter本の基本部分を纏めたようなもの

横内さんの本が好きな人ならばGunter本も読んでとても楽しめると思う
ちなみにCPDTとは直接には無関係

90年代前半は社会全体もバブルの時代だったがフォーマルセマンティックスの分野も次々に良い本が出版されて一種のバブルみたいだったなあ
最近、そういう本の出版が少なくなって（フォーマルセマンティックスの出版バブルの後、型理論関係の本の出版が少し多かった時期はあるが）寂しかったので
CPDTが出るのは本当に楽しみ

>>57 トンクス
>>56 女子大生の夏休みワロタwww でも俺も楽しみwww

おねえさんの説明でさっぱりわからなかった俺用メモ

ttp://sunak2.cs.shinshu-u.ac.jp/~miyao/UD/Subjects/Kouri/logic.htm

とてつもなく基本的な質問ではないかと思うのですが、

Definition prop1 : forall (A : Prop), A \/ ~A.

のような、仮定のない証明はどのようにすればいいのでしょうか？

プログラミングCoqの練習問題には
問3. forall (P : Prop), ~(P /\ ~P)
という、→のない証明の回答例がありますが、これは
一番外のnotを展開することで→Falseが発生しているのでそれを
使っているようです。

なにぶんCoqどころか論理学自体初心者なものですみません。

Require Import Classical.
Definition prop1 : forall (A : Prop), A \/ ~A.
apply classic.
Defined.

こらｗ

Require Import Classical.

Theorem eom : forall P:Prop, P \/ ~P.
intro P.
apply NNPP.
intro H.
elim H.
right.
intro p.
elim H.
left.
assumption.
Qed.

こんな知ってるか知らないかだし
CoqIDEなるProofGEneralなり使って一行ずつ動かしながらどうGoalが変化するか観察するのがいいよ
俺はそうやって覚えた

>>63
回答ありがとうございます。

「Proof-editing mode であそぼう」レベルの今の自分にはとても立ち向かえない
課題だったということがわかりました．．．

しかし、~(P /\ ~P) は割とあっさりできるのに、A \/ ~Aはいろいろ大変なあたり、
独学で自分で課題を決めて取り組む、というのがやりにくいですね。どの程度大変な
ものに向き合ってるのか、まだ読めないです。

学校で勉強したい・・・

流石に直感主義論理とNDの初歩ぐらい知っておかないとこの問題を自力で解くのは難しいかもしれない
とはいうものの簡単な数理論理学の教科書一冊読めばそれぐらいの力付くと思うけどね
独学なら

Coq'Art
http://www.labri.fr/perso/casteran/CoqArt/index.html

Software Foundations
http://www.cis.upenn.edu/~bcpierce/sf/toc.html

cpdt
http://adam.chlipala.net/cpdt/

あたりがおすすめ
Coq'Art買えないというならSoftware Foundationsからかな
coq'artも課題の答えが著者のサイトで見れるから独学には向いてると思う

Coq'Art 中国語版あんのかよ。

専門書もサイトもソフトも、日本語訳って以前より減ってない?

>>65
ありがとうございます。とりあえずSoftware Foundationsから読み始めてみます。

Coq'Artが届いたらそちらにシフトしてみます。

もしよろしかったら、直感主義論理とかNDにたどり着けるような日本語の本も
ご教授いただけますか？
ちなみに今読んでいるのは、野崎先生の「不完全性定理（ちくま学芸文庫）」です。
とまぁ、こんなレベルなのですが・・・

持ってるだけですが、「論理と計算のしくみ」とか「圏論による論理学」とか
「計算可能性とラムダ計算」は手元にあります。
が、「この辺の本を読む前に読んでおくべき本があるはずだぁ」というのが素直な
感想です．．．

>>66
悲しいですがこれが現実なんですかね・・・
これ以上差をつめられないように（開かないように？）、がんばらないと。

>>67
その三冊なら論理と計算のしくみを読むのがいいかな
というかその本の演習問題に全く同じような証明問題があるから

>>68
今見直してみると、「論理と計算のしくみ」っていい本ですねこれ。
買ったときはラムダ計算のところが読みたかったので後半しか見てなかったのですが、
前半に論理学の基礎がてんこ盛りに整理されてますね。
一緒に取り組んでみます。ありがとうございます。

サイモン博士とニューウェル博士が最初の定理証明システムを手がけたときのことを想像してみる。
論文を読んだ人はプリンシピア・マセマティカを横に並べて読み進んだんじゃないだろうか？

小学校レベルでも高校レベルでもかまわないから、
数学の教科書と並行してCoqの基礎を学んでいけるテキストが欲しい。

時間があったんで、

Software Foundations
http://www.cis.upenn.edu/~bcpierce/sf/toc.html

の「Basics」の章を全訳したんですけど、
公開するとまずいですよねぇ・・・・きっと。

巷にもう少し日本語の解説があれば普及も進むのでは
ないかと思うのですが。

Copyright書いてないね。
型理論の人たちは結構フリーで膨大なページ数のテキスト公開してるから聞いてみれば?

>> 公開するとまずいですよねぇ・・・・きっと。

原文のドキュメント作成者たちは無償で公開している。多くの方に読んでもらうためだ。

それを翻訳して公開するのに喜びこそすれ、嫌とは言わないだろう

もちろん、ドキュメント作成者の了解が前提になるが。

メールを出してみるべき。

ペンシルバニア大学の先生ですよね。ビビる・・・

CPDTは、「出版間近」って感じなんでさすがにまずそうですが、
Software Foundationsのほうは、これをどうしたいのか、なんで
公開しているのか、どこにも書いてないんですよね。

メール出してもし許可がもらえたら、もう一度見直してボチボチ
公開したいところです。

まぁ、「４０代オッサンの夏休み」になりますが。

>>74
> CPDTは、「出版間近」って感じなんでさすがにまずそうですが、
> Software Foundationsのほうは、これをどうしたいのか、なんで
> 公開しているのか、どこにも書いてないんですよね。

自分が担当している講義の為の資料を受講生以外の一般にも公開しているという事です。
このSoftware Foundationsに沿った形での講義をPierceさんらはやってますから。
（PierceさんのHPのTeachingの最初の科目、CIS500とかいう番号が付いてるやつです）

CPDTは明らかに本として出版するのを大前提として書かれてますし、本として読める単一ファイルの形でなっていますが、
こちらのSoftware Foundationsは少なくとも今の時点では紙に印刷される（か電子出版される）従来の書籍の形態にはなっていませんね。
マニュアルなどで良くあるWebページとリンクの集合体として現在は組織化されてますから、
当面は普通の書籍としては出版する予定はないように見えます。
もちろん、Pierceさんらが（少なからずが出版を最終目標とする）旧来型のPSやPDFの単一ファイルにしたものを
実は作っているが公開していないという可能性はゼロではありませんが、その可能性は少ないと思います。

>>75

よく見ると、前書きにその辺のことがチラッと書いてありましたね。跳ばして読んでました。

これによると、この文書を誰かが自分の講義に使うことは否定してませんね。
使う場合には連絡しろとも書いていない。

「ただ、そうするとどこかに直したいところや加筆したいところが出てくるだろうから、
そういうのがあったら連絡してね。subversionのレポジトリ教えてあげるから。」

てなことは書いてありますが。

この雰囲気だと、翻訳の公開を拒絶されそうな気配は無さそうですね、なんとなく。

あーそれだめだわ。
断られるわ。

>>75
coqdocだからPDFにはすぐ出来る。-pdf付けるだけ。

昨夜、Pierce先生にメールをしたところ、長文のお返事をいただき、
日本語版の公開を快諾していただきました。

ただ、公開間近の最新版がもうすぐ出来上がる予定で、今のとだいぶ変わって
いるので、それも考慮したほうがいいのではないのではとのことです。

ということなので、最新版とその差分が見られるよう、レポジトリの
アカウントを作っていただくことになりそうです。

とりあえず最新版を見せてもらって、あんまり変わってないようなら
今手元にあるのをさっさと公開しようと思っています。

やるじゃん

.vへのコピペに飽きてきたので暫定公開。

http://www.randmax.jp/sf/Basics_J.html

フォーマットがややオリジナルと異なりますが、二つ理由があります。
　1. 僕がCSSを少しいじっているため。主に日本語対応。
　2. sfのチームはcoqdocをカスタマイズして使っており、それを入手していないため。

単に「お前の翻訳はヘタ」というような批判は勘弁してください。「手伝ってください」としか言いようがありませんので。

具体的な「ここはたぶん誤解してる。正しくはこう」とか「この単語は普通こう訳す」というようなお話は歓迎します。
ここでやるのが不適切なようでしたら、どこかほかのところに場所を借りてもいいかと思っています。

「オレにもやらせろ」はもちろん「オレにやらせろ」も歓迎です。僕にとって翻訳は趣味でも仕事でもないので、日本語の文書が最初からあるなら（誰かが作ってくれるなら）、僕もそれに乗っかりたいぐらいです。

Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・

>>81
翻訳Webページに、参加方法やリポジトリ閲覧方法や訳文投稿窓口を含めておくと、敷居が低くなるかもしれない。
たとえばwikiのようなものとか。

>>81
> Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・

最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。

>>82の案を推す
俺もこのページは読んだことあるから多少は助力できるかも

>>81
誤字をなおしたりとかならお手伝いできるから、>>82みたいにしてくれるとうれしい

みなさんいろいろありがとうございます。

Wikiについては、だいぶ更新がとまっているCoqWikiがなるものがあるので間借りすることも考えたのですが、
たいしたコストがかかるわけでもなさそうなので、どこか別に借りてみようかと思います。
準備ができたらそちらも追って公開します。

とりあえず明日には、Basicsの全体を暫定公開できると思います。
そうこうしているうちにSVNレポジトリのアカウントが届くのではないかと。

なんだか長い旅になりそうですが、ひとつ気長にお付き合いください。m(_ _)m

>>83
>最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。

僕もそう思うんですけど、本当言うと学生さんに頑張ってほしいんですよね。
こういう日本で開拓の進んでない分野に切り込んで貢献する体験を若い人に沢山積んで欲しいと思うのです。
僕など成長したところで先が知れてますんで。

だからといって若い人に「お前がやれ」というのもかっこ悪い大人だと思うので、自分でやってしまったのですが。
どこかで誰かが「しまった！僕が先にやっておけばよかった！」と後悔してくれていればいいなと。

とりあえずWikiを借りてみました。

http://www16.atwiki.jp/sf_j/

特に制限などつけていませんが、できればWikiに参加してログインを行って書き込んでいただけると安心できます。

僕の身分は自己紹介のとこからリンクをたどっていくとわかるようになっています。
大した者ではありませんが、怪しい者でもありません。

皆様のご参加をお待ちしております。

>>87
『ソフィーの世界』、関係ねぇwww
これも何かの縁だと思って、正義論とか心の哲学とかも読もうぜ

今日いろいろ調べ物をしていて仰天しました。

僕が先月下旬ごろノートに一生懸命翻訳を書いている間に、
「プログラミング言語の基礎概念」という本が、サイエンス社から出版されていたのですね！

しかも著者は、ラクダ（OCaml）本の五十嵐淳先生。ペンシルバニア大でPierce先生と机を並べていたこともあるという。
一瞬、「Software Foundations」の翻訳が出たのかと思ったのですが、会社の帰りに日本橋丸善に寄って探すと、別の本でした。

とはいえ、内容的にはチョコチョコ重なっているところもあり（OCamlですが）、日本語で書き下されているものなので非常に読みやすいし、わかりやすいです。
これはお勧め。1850円というのもびっくりリーゾナブルです。

ここ見ているような人は内容的に目新しくないのかもしれませんが・・・

とりあえずwikiの下の方の広告をクリックしまくっておいた。

なんだそのブログみたいな文体は

>>90
お気遣い、とてもありがたいのですが、
Wikiの広告をクリックしていただいても僕には１円も入りません・・・・単にWikiサーバの運営費と運営会社の利益になるだけでだと思います。
もちろんクリックしても何の問題もないとは思いますが。

>>92
早とちりで失礼しました。

本日、日本語版を一応リリースいたしました。Pierce先生にもその旨連絡しました。

Basicsまでは、そこそこの完成度の翻訳になっているつもりですが、何かお気づきの点がありましたらWikiにお願いします。

僕自身もこれを翻訳した後、自分の日本語を読みながら一通り課題をやりましたが、
難易度が上がっていくペースがなかなかいい教材なのではないかと思います。

未来嬢の「プログラミングCoq」と併せてとりくんでもらえるといいかなと。

型定義、関数シグニチャを提供して、
ユーザーに関数の中身を定義してもらう枠組みを考えてるんだけど、
ある種の制約を守れば正しく動作する関数が定義できますよ、としたいんだけど、
そのときの制約として、
・関数シグニチャに沿っていること
・こちらで定義した補助関数のうち、絶対に使っちゃいけないものがある
・関数の中はCoqに通り、上2つの制約に矛盾しなければ何でもOK
というようにするには、どうしたらいいんでしょうか。
最初のは多分Classとして与え、
ユーザーにInstance化してもらえばいいんだけど、
2個目の条件が満されていることはどうやって確認したらいいんですかね?

確かextraction機構はプラグインみたいな形でコア部分と別だったから
Extractionする段階で、定義済みの関数の式木を舐めて特定の名前の関数を使用しているかいないかで判定とかは可能だと思う

RT @mzp #sfja http://proofcafe.org/sf/ SoftwareFoundation和訳(4章まで)

もしし

>> 60さん
あれ、Software Foundationsの場所変わったの？
作業場所もwikiからGithubに変わったみたいだけど、運営者かわったの？

wikiに説明が書いてあると思うが

>>githubの方は60さんに刺激を受けたfm forumの人がやってるやつで完全に二つは独立してるよ

>>101
なるほど。ありがとうございます。見た感じ今はgithubの方が勢いがあるのかな？

>>101
実際は、60が10月から忙しくなったのでProofSummit で協力をよびかけて、賛同者の作業がやりやすいようGithubに移行したということです。60もGithubに参加しています。

それは知らなかった説明ありがとう

>>103
うん？どういうこと？
二つは独立しているのではなく、作業場所が変更したってこと？
最新の作業情報はgithubのプロジェクトをみればよい？

>>105
そういうことです。
Github のほうが真(新)です。
Wiki のほうは、その事がちゃんと分かるように直しておきます。

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

@n_k28 魔理沙気持ち悪かったです。もう二度とやらないで下さい＾＾

(P -> Q) -> (~P \/ Q)
これの証明ができん。

ああ
~~((P -> Q) -> (~P \/ Q))
なら証明できるのか。
直観主義論理がどうとか俺にはちんぷんかんぷんだ…。

tauto.でおｋ

Inductiveな型TからT_rectが生成される原理がどうしてもわからないなあ。
誰か教えてちょーだいな。

#coq #inductive
>>112 例えば nat_rectならFixpointでも定義できるよ。
Variable P : nat -> Type.
Axiom fO : P O.
Axiom fS : forall n, P n -> P (S n).
Fixpoint nat_rect' n : P n :=
match n with
| O => fO
| S m => fS m (nat_rect' m)
end.

nat_rectぐらいなら、数学的帰納法なんてなじみがあるからなんとなくわかるけど、
例えば
Inductive sand (A B : Set) : Set :=
sconj : A -> B -> sand A B.
から作られるsand_rectなんかは、

sand_rect =
fun (A B : Set) (P : sand A B -> Type)
(f : forall (a : A) (b : B), P (sconj A B a b)) (s : sand A B) =>
match s as s0 return (P s0) with
| sconj x x0 => f x x0
end
: forall (A B : Set) (P : sand A B -> Type),
(forall (a : A) (b : B), P (sconj A B a b)) ->
forall s : sand A B, P s

となって、わかりそうなわからなそうな。上記のSetをPropにかえるともうお手上げ。
いったい何を理解すればいいのやら。どうか神様教えて。

>>114 nat以外のものも構造的帰納法を表しているだけ。
X_rectのたぐいは自作する必要はないから、関数定義は理解できなくても
型だけわかれば、使えるからそれで いいと思う。
このX_rectがどのように自動生成されるか、Coqの内部のアルゴリズムが
知りたいならば少し勉強が必要かもしれないけれど、普通に使う分にはいらないでしょ。

>>115
ということは、構造的帰納法について、私が理解している以上に何か深いこと、
あるいは、もっと詳しいことがあるということでしょうか。論理式の定義に従って
帰納的に何かを証明するとか、そんなことは何の苦もなく理解してきましたけど、
上記>>114のsand_rectなんぞは、なぜそうなるのかいまひとつわからないのです。
また、sandの定義中のSetをPropにかえたものをpandとすると、pand_rectは
sand_rectのSetをPropにかえただけのものとは異なります。ますますわかりません。
もし構造的帰納法について詳しく書かれた文献等あったらご紹介いただけないで
しょうか。

少しだけわかってきました。sand_rectの型の部分がそうなりそうな気もしてきました。
すると、本体（t:Tにおけるtのこと）がなぜそのように構成されるのか、という疑問に
なりますが、それは半分は発見的経験的に考えないといけないのでしょうか。

また、pand_rectに関しては、sand_rectの(P : sand A B -> Type)の部分が
なぜか(P : Type)になっている。つまりsand_rectにあるPはsand A Bを引数にとってたのに、
pand_rectにあるPはpand A Bを引数にとらなくなっている。
これさえ認めればsand_rectとpand_rectの違いは説明できます。これはなぜなんでしょう？

少しずつわかってくるにつれて、Coqとは直接関係ない気もしてきたのですが、
どなたか教えてくださるか、もしくは良い文献の紹介等していただけないで
しょうか。

自然数の定義を例に話します。
（１）Oを自然数とする。
（２）nを自然数とするとき、S nも自然数とする。
（３）上記（１）（２）によって定められるもののみを自然数とする。
といった具合に自然数を定義することができますが、この（３）をどのように
形式的に表すかをもっと詳しく理解すれば、私の疑問が解けるような気がしてき
ました。

どうか偉い方々、よろしくお願いいたします。

Coq'Artの14章あたりにもある程度載ってるんだけども形式的な説明というわけでは無いね

論理や集合論の命題と型付きラムダ計算の式が1対1対応するっていう性質を使ってるってことは聞くけど
再帰型の定義が計算体系に及ぼす影響が対応する論理体系にどういう影響与えるかとか
そういうのはよくわからない・・・
せいぜい構築子の無い型の値を仮定するのとFalseぶち込むのが対応してどちらも滅茶苦茶になるとか、そういうのぐらい
::=はiffに対応するとか|は排他論理和に対応するんだなぁというのは経験則でみえてくるけども

×型付きﾗﾑﾀﾞ計算の式
○型付きﾗﾑﾀﾞ計算の型

>>118 構造的帰納法に関しては俺はTAPLで勉強したな。あの本は丁寧で
わかりやすい。

>>119-121
いろいろと情報提供ありがとうございます。いまはCoq'Artの14章で奮闘中です。もともと英語が苦手
なのですが、贅沢は言ってられません。TAPLって、Benjamin C. Pierceの「Types and Programming
Languages」のことですよね。あたってみます。（砕けたりして。トホホ）

http://proofcafe.org/sf/ に日本語訳を上げて下さっている方の書き込みがあったので、ここに書いておきます。

一部訳に打ち間違いがあります。どこに言ったら良いのかわからないので、ここに書いておきます。

http://proofcafe.org/sf/Poly_J.html

の[マップ（Map）関数]のちょっと上に「理宇土」とあります多分「リスト」の誤変換だと思います。

この訳のお陰で大変楽して勉強できてます。ありがとうございます。

http://proofcafe.org/sf/Poly_J.html
の
rememberタクティック
のちょっと前に「なるべくintrosを使うタイミングを送らせ」の「送らせ」は「遅らせ」だと思います。

よろしくお願い致します。

訳ありがとうございます。

報告するならgithubのissue tracker
https://github.com/sfja/sfja/issues
か
wikiの専用ページ
http://www16.atwiki.jp/sf_j/pages/49.html
でやるほうがいいと思うよ

>125
ありがとうございます。そっちに書いときます。

うわーはずかしいtypo。直しておきます。レポート感謝。

0 と 1 だけのタイプを作りたいと思い

Inductive my : Type := O : my .
my is defined
my_rect is defined
my_ind is defined
my_rec is defined

は上手く動作するのですが

Coq < Reset my.

Coq < Inductive my : Type := O : my | 1 : my .
Toplevel input, characters 32-33:
> Inductive my : Type := O : my | 1 : my .
> ^
Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).

Coq < Inductive my : Type := O : my | (S O) : my .
Toplevel input, characters 32-33:
> Inductive my : Type := O : my | (S O) : my .
> ^
Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).

となって上手く定義できません。どうやれば 0 と 1 だけのタイプを定義できるんでしょうか。

Inductiveで列挙するのはコンストラクタの名前とその型。
値を並べられるわけではない。

1を名前に使えない
Inductive my : Type := O : my | one : my .
ならいい

O(:nat)もコンストラクターなんじゃない？

なんか >>60 が変な扉を開いてしまったかもしれない。

「関数型ガール」
http://www16.atwiki.jp/sf_j/pages/56.html

>129
>130
>131
>132

回答ありがとうございます。

O を起点として

O と (S O) だけの Typeとか

O と (S O) と (S (S O)) だけの Type とか

O と (S O) と (S (S O)) と (S (S (S O))) だけのTypeとか

...

を作りたかったのですが、そうするにはどういうコマンド入れたら良いのでしょうか>

レベル低い質問ですみません。

Inductive my : Type := O : my | S : my -> my.

こうしちゃうと O と (S O)だけじゃなく (S (S O))も myタイプになってしまうのでどうしたらよいのかわかりません。

>>134
証明を引数として取るコンストラクタを使うとか

Require Import Arith.

Inductive my (n:nat) : Set :=
| myO : my n
| myS a : a <= n -> my n.

Section my1.
Let my1 := my 1.
Definition my1_0 : my1 := myO 1.
Program Definition my1_1 : my1 := myS _ 1 _.
End my1.

Inductive Fin : nat -> Type :=
| FinO n : Fin (S n)
| FinS n : Fin n -> Fin (S n).

というのをcoq-clubで見た。

ネット務

>>135
>>136

ありがとうございました。
またやってみます。

Software Foumdationsの翻訳がとりあえず最後まで終わりました！

というわけでお願いなのですが、読んでください。

で、誤字脱字誤訳など指摘頂けると助かります。

結局ろくな証明できないなｗ

質問です。
まえもって証明したLemmaを再利用してゴールに適用する方法をおしえてください。

applyを使いましょう