集合論に基づいた言語を作りたいat TECH集合論に基づいた言語を作りたい - 暇つぶし2ch■コピペモード□スレを通常表示□オプションモード□このｽﾚｯﾄﾞのURL■項目テキスト845:１ 15/01/21 20:33:19.47 83hEDbKu.net 片山さんの模範解答うｐ希望 846:片山博文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. 847:１ 15/01/21 22:49:05.70 83hEDbKu.net ふーむ。確かに片山さんのほうが自然な証明ですな。 848:片山博文MZ ◆T6xkBnTXz7B0 15/01/23 02:17:55.54 22/uje4h.net 布教のために数学板でも展開するぞ。 【Coq】コンピューターで証明しよう【コック】･2ch.net http://wc2014.2ch.net/test/read.cgi/math/1421944863/ 849:デフォルトの名無しさん 15/10/21 21:08:46.20 qGjQS7QU.net http://connect4.game-solver.org/?pos= 850:デフォルトの名無しさん 15/10/21 21:49:58.99 kanshW5q.net ほう、4並べのソルバですか。面白い なぜこのスレなのかは気にしないでおこう thx 次ページ最新レス表示レスジャンプ類似スレ一覧スレッドの検索話題のニュースおまかせリストオプションしおりを挟むスレッドに書込スレッドの一覧暇つぶし2ch