15/01/04 21:45:09.09 izkph8nP.net
>>786
「Coq tutorial PDF」で検索
788:デフォルトの名無しさん
15/01/04 21:59:00.42 7jAGFdTv.net
URLﾘﾝｸ(coq.inria.fr)
これ？
結構分量ありますね。
789:１
15/01/06 00:03:50.53 iQ4UNt/k.net
Coqで任意の自然数nに対してn*(n+1)が偶数であることを証明しようとしたがどうしてもできない。
だれかHELP.
790:１
15/01/06 00:34:25.70 iQ4UNt/k.net
定義はこれで。
Theorem t:
forall (n:nat),exists m , (n*(n+1) = 2 * m).
791:デフォルトの名無しさん
15/01/06 05:55:25.49 Gduz5N96.net
偶数+1は奇数
奇数+1は偶数
遇数*奇数も奇数*遇数も遇数
自然数は奇数か偶数かどちらかである
792:１
15/01/06 21:04:14.92 iQ4UNt/k.net
「nが奇数ならn+1は偶数」を証明しようとして詰まってる。
Require Import Even.
Lemma l:
forall (n : nat), odd n -> even (n+1).
intros.
induction n.
simpl.
apply even_S.
これでodd 0とかいうのが出てくるけど、ここからどうしていいかわからない。
793:１
15/01/06 21:10:59.52 iQ4UNt/k.net
「自然数nに対してn*(n+1)が偶数である」
本題のこっちはここまで進んだ。
Require Import Even.
Theorem t:
forall (n:nat), even (n*(n+1)).
intros.
apply even_mult_aux.
794:１
15/01/06 23:17:17.43 iQ4UNt/k.net
Coq難しすぎんよ～
もう寝る。
795:１
15/01/07 19:22:04.95 DdlkDaa+.net
URLﾘﾝｸ(www.iij-ii.co.jp)
このページによるとforall (P : Prop), P \/ ~ Pは証明できなんだそうだ。
forall (n:nat), even (n*(n+1)).も証明できないのかもしれないな。
796:デフォルトの名無しさん
15/01/07 20:14:30.38 zH4wOwdk.net
1に餌を与えないでください。
>>425>>559>>655-665
797:1
15/01/07 21:02:58.84 DdlkDaa+.net
odd 0 -> Falseは証明できたっぽい。
これをどう活用すればいいのかわからない。
Lemma l2:
odd 0 -> False.
apply not_even_and_odd.
apply even_O.
798:デフォルトの名無しさん
15/01/08 15:50:20.90 FouB2F9v.net
S
799:デフォルトの名無しさん
15/01/08 18:29:26.11 qFLJfmjp.net
O
800:デフォルトの名無しさん
15/01/08 19:09:01.13 XNa5H7Wz.net
S
801:１
15/01/08 20:07:08.21 9tH8cNHX.net
ハルヒか？
802:１
15/01/08 22:27:11.24 9tH8cNHX.net
そもそもodd n -> even (S n)って定義そのものなんだよなぁ。
803:1
15/01/11 19:52:52.15 zln55Xsd.net
ギブアップ。
だれか正解しってたら教えて。
804:1
15/01/13 18:35:43.03 7YFvdf+i.net
片山さん答え知ってたら教えて
805:デフォルトの名無しさん
15/01/13 20:23:10.10 ElusS0xD.net
ｽﾚﾘﾝｸ(tech板:23番)
> 23 名前：片山博文MZ ◆T6xkBnTXz7B0 [sage]： 2015/01/13(火) 18:53:35.00 ID:gURRjQHf
> 私はお下品
806:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 21:52:38.35 gURRjQHf.net
ヒント。
Require Import Even.
Lemma eSr: forall n:nat, even (1 + n) -> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.
807:１
15/01/13 22:46:33.61 ld5ZWEPI.net
Lemma l : forall (n:nat), even (1+n)-> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.
apply odd_S.
apply even_O.
Qed.
こう？
nを偶数と奇数に場合分けする方法がわからんとです。
808:１
15/01/13 23:04:11.48 ld5ZWEPI.net
even(1+n)にeven(1+n) -> odd nをapplyして odd nにならんのか？
よくわからん。
809:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 23:09:34.67 gURRjQHf.net
Lemma oS: forall n:nat, even n -> odd (S n).
intros.
apply odd_S.
apply H.
Qed.
810:１
15/01/13 23:38:41.86 ld5ZWEPI.net
証明済みのLemmaの活用の仕方がわからんです。
applyじゃないの？
811:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 23:39:26.18 gURRjQHf.net
replace (even (S n)) with (odd n).
apply even_or_odd.
もう少しだな。
812:1
15/01/14 00:05:14.20 upPMt0VH.net
A=Bを示したかったらA->BかつB->Aで方針あってますか?
813:１
15/01/14 00:09:20.78 upPMt0VH.net
もう寝ます。
また明日よろしくお願いします。
814:片山博文MZ ◆T6xkBnTXz7B0
15/01/14 19:03:17.31 lWtQJ7uI.net
聞きたいことがあれば、俺の掲示板に来いよ。待ってるぜ。
815:片山博文MZ ◆T6xkBnTXz7B0
15/01/15 14:58:59.94 OiYOltU9.net
URLﾘﾝｸ(katahiromz.bbs.fc2.com)
816:デフォルトの名無しさん
15/01/15 18:04:49.36 UYCK2hGt.net
>>814-815
1がそっちに行ってくれればいいけど。
1はCoqとか本当はどうでもよくて、このスレに書くこと自体が目的になってるだろうから・・・
817:デフォルトの名無しさん
15/01/15 20:46:59.13 QgJ4DA/V.net
>>816
雑談はこちらの412に書いてるな。
戻ってくるなよ ＞1
818:１
15/01/15 21:04:35.89 RCkerH2f.net
お前らこのスレが伸びちゃ困る理由でもあるのかｗ
819:デフォルトの名無しさん
15/01/15 22:49:41.86 5ppshwSd.net
>>818
1が「集合論に基づいた言語を作る」話をしないからな。
>>425>>559>>655-665
どうせエサをくれるのは片山博文MZだけなんだから、ずっとあっちに行ってろよ。
820:1
15/01/15 23:03:37.94 RCkerH2f.net
このスレはお前らで盛り上げてくれてもかまわないんだぜ？
821:デフォルトの名無しさん
15/01/16 00:08:32.30 q80wbXpz.net
このスレ見てるの結構楽しい（煽りとかではなくいろんな話が出てくるし）から盛り上がって欲しい
822:１
15/01/16 00:10:36.55 tbQRRWp6.net
できたっぽい。
片山さんに教えてもらったページみた。
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.
Coq相当親切なチュートリアルがないと勉強できんわ。
どのタクティク使えばいいのかとかわからんすぎる。
823:片山博文MZ ◆T6xkBnTXz7B0
15/01/16 01:05:01.69 IPI8U3lP.net
>>822
なかなかやるじゃん。
ついでに「片山QZの定理」の証明でもやってみる？
片山QZの定理
URLﾘﾝｸ(katahiromz.web.fc2.com)
824:１
15/01/16 18:38:49.28 tbQRRWp6.net
MZとかQZとかって何なの？
別にいいんだけど。
片山QZの定理はなんかえらい難しそうなのでやめとく。
825:片山博文MZ ◆T6xkBnTXz7B0
15/01/16 18:52:49.05 IPI8U3lP.net
QZというのはC/C++宿題スレに生息している人だよ。
そうだな。2n＝n＋nの証明なんかどうかな？ 楽勝？
826:１
15/01/16 19:09:16.59 tbQRRWp6.net
掛け算の定義がどこにあるのかわからん。
証明もいいけどコードの自動生成のほうが面白そうかな～
827:片山博文MZ ◆T6xkBnTXz7B0
15/01/16 22:32:01.39 IPI8U3lP.net
>>826
英語では、掛け算がmultiplicationで、自然数がnatural numbersだろ？
それを略すればmul,natになるだろ？
SearchAbout mul.
SearchAbout nat.
で検索できるから。
828:１
15/01/16 23:47:30.80 tbQRRWp6.net
>>827
結構むずかしい。
仮にできたとしても時間かかると思う。
829:１
15/01/17 00:13:16.15 e9PIZEl5.net
ぶっちゃけCoqやってると無限に時間を吸われる可能性がある。
早めに身を引いた方がよさそうかな～とも思う。
830:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 01:27:28.08 PPUSm5YO.net
数学に基づいた言語としてCoqは最適の例かと思われたが、御気に召さないとはこれ如何に。
では、そなたはどのような言語が希望か申し上げてみよ。
831:１
15/01/17 02:12:55.60 e9PIZEl5.net
いや～確かにCoq面白いんだけど。
勉強するのに時間かかり過ぎるっていうか
もうちょっと市民権を得て入門書とか充実してからの方がいいかな～と。
証明も紙なら簡単にできることが結構難しかったりで、
実利を得るところまで勉強進めるのがしんどい。
実用までいかなくてただのパズルで終わりそう。
Coq参考になるところは多いと思うんだけどね。
どこまで時間費やすか見極めたほうがよさげ。
片山さんはCoqにどの程度手ごたえ感じてるの？
832:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 02:59:53.32 PPUSm5YO.net
麿は、この素晴らしきCoqを使えば、不具合のないソフトウェアが作れると見ては、
これをマスターすれば世界征服も夢ではないと、そのような所存でおじゃるよ。
833:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 03:31:41.14 PPUSm5YO.net
Coqと人工知能を組み合わせたら……、金融取引に活かせば……とか楽しい妄想が広がるでおじゃる。
834:１
15/01/18 22:30:12.77 Pnbu8M/I.net
人工知能といえばdeep learningとかいうのが流行らしいんだが。
835:１
15/01/20 23:02:01.33 RE29itzd.net
2n=n+nはomegaで一発っぽい。
omegaなしだとどうやるかわからん。
836:デフォルトの名無しさん
15/01/21 01:37:31.40 +/NZ76QF.net
1に餌を与えないでください。
>>425>>559>>655-665
837:片山博文MZ ◆T6xkBnTXz7B0
15/01/21 08:55:01.51 y20qOxOP.net
n＝1×nを使う
838:1
15/01/21 19:32:48.10 83hEDbKu.net
途中よけいなことしてるかもだができたっぽい。
Require Import Arith.
Theorem t:forall n:nat,2*n=n+n.
intros.
replace (2*n) with (n*(S 1)).
symmetry.
replace (n+n) with (n*1+n).
apply mult_n_Sm.
replace (n*1) with (1*n).
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
apply mult_comm.
apply mult_comm.
Qed.
839:１
15/01/21 19:37:49.38 83hEDbKu.net
Coqは一日一時間までにする。
それ以上は自重。
840:１
15/01/21 20:33:19.47 83hEDbKu.net
片山さんの模範解答うｐ希望
841:片山博文MZ ◆T6xkBnTXz7B0
15/01/21 22:08:31.55 OPHJ2hAi.net
>>840
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.
842:１
15/01/21 22:49:05.70 83hEDbKu.net
ふーむ。確かに片山さんのほうが自然な証明ですな。
843:片山博文MZ ◆T6xkBnTXz7B0
15/01/23 02:17:55.54 22/uje4h.net
布教のために数学板でも展開するぞ。
【Coq】コンピューターで証明しよう【コック】･2ch.net
ｽﾚﾘﾝｸ(math板)
844:デフォルトの名無しさん
15/10/21 21:08:46.20 qGjQS7QU.net
URLﾘﾝｸ(connect4.game-solver.org)
845:デフォルトの名無しさん
15/10/21 21:49:58.99 kanshW5q.net
ほう、4並べのソルバですか。面白い
なぜこのスレなのかは気にしないでおこう
thx
846:デフォルトの名無しさん
16/05/01 11:01:21.14 tKi6j9CT.net
匿名通信（Tor、i2p等）ができるファイル共有ソフトBitComet（ビットコメット）みたいな、
BitTorrentがオープンソースで開発されています
言語は何でも大丈夫だそうなので、P2P書きたい！って人居ませんか？
Covenantの作者（Lyrise）がそういう人と話したいそうなので、よろしければツイートお願いします
URLﾘﾝｸ(twitter.com)
ちなみにオイラはCovenantの完成が待ち遠しいプログラミングできないアスペルガーｗ
The Covenant Project
概要
Covenantは、純粋P2Pのファイル共有ソフトです
目的
インターネットにおける権力による抑圧を排除することが最終的な目標です。 そのためにCovenantでは、中央に依存しない、高効率で検索能力の高いファイル共有の機能をユーザーに提供します
特徴
Covenant = Bittorrent + Abstract Network + DHT + (Search = WoT + PoW)
接続は抽象化されているので、I2P, Tor, TCP, Proxy, その他を利用可能です
DHTにはKademlia + コネクションプールを使用します
UPnPによってポートを解放することができますが、Port0でも利用可能です(接続数は少なくなります)
検索リクエスト、アップロード、ダウンロードなどのすべての通信はDHT的に分散され、特定のサーバーに依存しません
ｃ