読んだ本の数：5冊 読んだページ数：1538ページ狼と香辛料〈14〉 (電撃文庫)相手の心に踏み込んでいく勇気読了日：11月03日 著者：支倉 凍砂もいちどあなたにあいたいな久々に素子節を堪能した気がする。"卑怯階級"は刺さるなぁ(- -;読了日：11月07日 著者：…

リストに関する証明でもinductionが使えるよという話。まずはリスト中に指定した数がいくつあるかを数えるcountという関数を定義。 Fixpoint count n l := match l with nil => 0 | a::tl => let r := count n tl in if beq_nat n a then 1 + r else r end.…

ex.1 addの定義は以下。 Fixpoint add n m := match n with 0 => m | S p => add p (S m) end.最初は下記のように書いた。 Lemma ex1' : forall n m, add n (S m) = S (add n m). Proof. induction n. intros m. simpl. reflexivity. rewrite IHn. reflexivi…

4.2 タイトルの"Stronger Statements"ってのはより厳密な命題って感じですかね？命題で使われている関数がいくつかのパターンマッチで定義されている場合は、成立すべき初期段階が複数必要ですよという話でいいのかな。例で使われるのはevenb。定義は以下 Fi…

4章は自然数を扱った証明でよく使われるtacticの紹介。 4.1 まずはinductionというtactic。こいつは数学的帰納法ってやつですね。 sum_nは2章で定義していて、 Fixpoint sum_n n := match n with 0 => 0 | S p => p + sum_n p end.ということで数学的帰納法…

ということでexerciseをやってみた。 ex.1 まずは定石に従い、introsすると 1 subgoal A : Prop B : Prop C : Prop H : A /\ B /\ C ============================ A /\ BHをさらに分割するためにdestructを適用。 1 subgoal A : Prop B : Prop C : Prop H1 …

3.3.2 rewrite 次はrewriteというtactic。 式変形だと思えばよいかな。左辺を式変形して右辺と同形になることを示すというわけ。 まずは分配法則を適用してみる。分配法則を表す定理は何かを探すのにはSearchRewriteというコマンドが使える。 SearchRewrite …

3.3 引き続き、いろんなtacticの例。 演算子/\に対して左辺と右辺に分割を行う場合は、3.2で出てきたように destruct H as [H1 H2]という形でdestuctというtacticを適用したけど、\/に対しては destruct H as [H1 | H1]と分割後の仮定を表すシンボルの間に|…

読んだ本の数：12冊 読んだページ数：2782ページバカとテストと召喚獣 (1) (角川コミックス・エース 256-1)読了日：10月04日 著者：夢唄,まったくモー助バカとテストと召喚獣 (2) (角川コミックス・エース 256-2)読了日：10月04日 著者：夢唄,まったくモー助…

いよいよ本題の定理証明へ。 3.2 Lemma hoge : … で証明すべき式を宣言。hogeは式につけられる名前。証明が完了すれば以後定理としてhogeの名前で参照できるようになる(らしい)。 Propは命題、/\は論理積を表してる。ということで論理積演算で交換律が成り立…

2.1 定数の定義 Definitionで定数定義というかbindですね。関数をbindするには下の略記が使えると。 2.2 条件式 ブール値を扱うにはBoolをImportしておく。 あるデータ型に対してどんな関数が定義されているかは、SearchやSearchAboutで調べられる。 2.3 自…

Checkは定義を表示。 Eval compute in ex でexを評価 という解釈でいいのかな。

定理証明器のひとつ、Coqをちょっといじってみようかと思い立ったので、この辺を参考にして、とりあえずCoq in a Hurryを写経してみようかと。

読んだ本の数：7冊 読んだページ数：1449ページストーリー・セラーメタ構造だったり、全体的に重い色調だったりで、有川作品としては異色作と言えるのではないかと。でも、描かれる夫婦の関係はやっぱりベタ甘読了日：09月01日 著者：有川 浩図書館戦争LOVE&…

読んだ本の数：8冊 読んだページ数：2634ページ 魔法使いの弟子たちラストがなぁ。読了日：08月04日 著者：井上 夢人あるキング天才の悲劇を淡々と綴った中編。王にならざるを得なかった悲劇読了日：08月05日 著者：伊坂 幸太郎ダイナー吐き気を催すほどの残…

読んだ本の数：11冊 読んだページ数：2127ページ 加藤直之グイン・サーガ画集図書館で見かけて思わず手に取ってしまった。当時、グインのみならずSF絵といえば加藤さんの絵だったなぁ。直筆のグインのラフ画は今でも宝モノです読了日：07月04日 著者：加藤 …

08:33 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/twit/dnt/ 13:02 豚カツ、サラダ、冷奴、味噌汁、ごはん。#lunch 13:05 蒸し蒸しでいや〜んな…

10:46 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/twit/dnt/ Powered by twtr2src

00:37 やっつけで月曜の資料作り。これ使ってみた http://j.mp/aYNBFX HTML書くの久しぶり 11:31 気になる RT @kawade: 放送は7/9の何時からなのかな？ RT @kurokikoichi: これは楽しみすぎる。YouTube - 宇宙犬作戦 http://bit.ly/aiUa01 11:33 .@dff_Click…

08:32 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/twit/dnt/ 08:38 6月のまとめ http://bit.ly/dggndT 15:56 おっ、ピカピカ、ゴロゴロ来た。 1…

読んだ本の数：10冊読んだページ数：2103ページウルトラヘヴン (1) (ビームコミックス)さしのべられた手は現実 or 幻想？ 続きも読もうっと。読了日：06月02日 著者：小池 桂一訳者解説 -新教養主義宣言リターンズ- (木星叢書)本文読みたくなる。朝日の書評…

08:33 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/twit/dnt/ Powered by twtr2src

00:44 今のなに？ 00:51 緊迫した試合展開を和ませるw RT @tsubuneko: ダンディーに足を組んで座る猫:ザイーガ http://bit.ly/b7SYW5 #neko 00:55 いや、別に我々を代表しているわけではないと思うが 01:11 .@dff_ClickBokin つぶやくことで無料で1円を募金…

08:11 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/twit/dnt/ 08:12 コーヒー、熱っ 13:25 京風がんもうどん、サラダ。#lunch 15:02 RT @junkudo…

08:35 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/twit/dnt/ 13:10 チキンカツ、サラダ、里芋の煮ころがし、味噌汁、ごはん。#lunch 17:38 目視…

10:41 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/twit/dnt/ 11:50 神龍？ http://movapic.com/pic/201006271150094c26bc61ee2e0 21:42 そうい…

00:27 タモリ倶楽部、ミキシングはラーメンに通ずる？w 00:37 Gate Reverb、流行ったよなぁ 11:04 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/t…

08:04 .@dff_ClickBokin つぶやくことで無料で1円を募金できます。「宮崎口蹄疫被害支援ツイッター募金」にご協力ください。【ケータイ可】 http://www.dff.jp/ct/twit/dnt/ 08:20 #nowplaying Pioneers of Aviation/Paradox Hotel by THE FLOWER KINGS 08:2…

08:19 #nowplaying Sisters/Road Salt One by Pain Of Salvation 08:25 #nowplaying Of Dust/Road Salt One by Pain Of Salvation 08:28 #nowplaying Tell Me You Don't Know/Road Salt One by Pain Of Salvation 08:31 #nowplaying Sleeping Under the Star…

01:18 口は災いの元つうか言い出しっぺの法則。まぁ、旗振るぐらいならやりますけども。 08:41 Jordan Rudessがプロデュース(?)したiPadアプリ http://ja.audiofanzine.com/other-virtual-synth/morphwiz/morphwiz/news/a.play,n.1528.html 08:44 .@dff_Clic…