2013-09-01から1ヶ月間の記事一覧
プログラム全体を一つの関数とみなしたり、関係の命題として表したり、自分には超難しい。証明もくそ長くなってきて手に負えなくなりつつある。そろそろ限界か。見たことないタクティックの使い方もやたら出てくんですが。 apply (H0 x) in H1. apply withを…
状態のところを読む。 Definition mystate : state := fun i => match i with | Id n => n // id nに対応するなんらかのnatを返すことが出来る。 end. Definition myid5 := Id 5. Eval simpl in update mystate myid5 10. (* Id 5に対応する値を 10にすると…
一日寝てた。 昨日のCoq 別に間違っておらんかった。間違ってたのは、omegaの使い方のようだ。 詰るところ使い方がわからん。 数値定数、加算(+とS)、減算(-とpred)、 定数の積算(これがプレスバーガー算術である条件です)、 等式(=と<>)および不等式( 論理…
仕事でPlay2を少し調べた。割と簡単そうかなと思う。nodejsなみに扱いやすそうかもしらん。 少しはscalaもやるかな。 今日のCoq Imp_J.vに入る。四則演算も満足に出来ないミニ言語のくせに、証明がいきなり長い。それに応じてTacticも大量に出て来た。それぞ…
短いRel_J.vを読んだ。 証明自体はそう難しいものは無いけれど、ほとんどサールの中国人の部屋状態。規則に従って何かを生成しているが、それが何を意味するのかほとんど分かっておりませぬ。 まとめ 関係Rが反射的とは、Xの任意の要素 xについて R x xが成…
Logic_J.vまで一応読了。分からん問題は答え見てもさっぱり分からん。 殊にappears_inがらみがまるで歯が立たなかった。途中 一つQed.を書き忘れて、 Error: There are pending proofsとかエラーが出てcoqcが失敗して難儀した。括弧の対応が取れてないような…
どうでもいい日記でも一日空くと大分やる気が落ちるね。カナ漢字変換に、uim-skkを使ってるんだけど、かなモードで記号が全角になるのが気になるんでどやってカスタマイズするのか調べてたら、uim自体ほとんどschemeで書かれてんのね。 カスタマイズは ~/.ui…
自分が理解したであろうところの証明オブジェクトの書き方。 XXX -> YYY := fun (H : XXX) => (fun (H1 : YYY) => H1) （← ここで YYY型の変数H1を返す関数を生成してそのまま実行。 ... YYY型の変数 を組み立てる何かの処理 ... ←上の行の関数の実行に対し…
どうもgithubで謎のハングルのかけらみたいなものが表示されるの は、githubで使用しているwebfontを表示出来ていないっぽい。 firefox 24.0 chromeだときちんと表示される。firefoxも、windowsだったら大丈夫である様子。
仕事が一区切りついてなりより。まあ9月から相当手抜いてました。すいません。 次の仕事の話を聞いてきたけど、かなり地雷臭いな。 なんとかProp_J.vを追加練習問題除いて終了。 Logic_J.vに入った。あいかわらず証明オブジェクト書くところで超モヤモヤして…
(* ev_ev_even *) Theorem ev_ev_even : forall n m, ev (n+ m) -> ev n -> ev m. Proof. intros n m E1 E2. induction E2 as [|n' E']. Case "E2 = ev_O'". simpl in E1. apply E1. Case "E2 = ev_SS n'". simpl in E1. inversion E1 as [|p E1']. apply IH…
やはり先週詰ってたとこで詰まる。全称記号つき命題を特定の値を伴って関数に渡したりする場合がよくわかっておりません。 Inductive ev :nat -> Prop := | ev_O : ev O | ev_SS : forall n : nat, ev n -> ev (S (S n)).で、コンストラクタ関数 ev_SSに何が…
午前中時間が空いた。 Inductive ok_day : day -> Prop := | okd_gd : forall d:day, good_day d -> ok_day d | okd_before : forall d1 d2 : day, ok_day d2 -> day_before d2 d1 -> ok_day d1. という型定義において、 okd_gd は（コンストラクタ）関数で…
台風が来てるなか、ぐーすか寝てた。 ベランダの鳩は健気にも強風のなかじっとしてた。でも抱卵の時期が長過ぎるような気がしないでもない。卵生きてんのか。 Inductive good_day : day -> Prop := | gd_sat : good_day saturday | gd_sun : good_day sunday…
ライブでした。歌う曲数は少なかったけど二部制だったんで疲れた。 おかんに始めて聞いてもらった気がする。もっとデカい声で歌えと言われた。
練習があったのでCoqの方は、あまり見てない。 明日本番だし。Prop_J.vを少し写経するも、何書いてあるかよく分からない。 (* ここで wednesday がOKであることを証明したいとしましょう。 証明するには2つの方法があります 1つめは原始的な方法であり、コン…
Inductive myprod (X Y : Type) : Type := mypair : X -> Y -> myprod X Y. Check myprod. (* <- 型を生む関数 *) Check myprod nat nat. (* <- (型関数 myprod が型引数 nat natを取って出来た)型 *) Check mypair nat bool 1 false. (* 構成子 mypairによ…
4章まで出て来たタクティーク一覧 intros: 仮定や変数をゴールからコンテキストに移す reflexivity: 証明を完了させる（ゴールがe = eという形になっている場合） apply... （in H）: 仮定、補助定理、コンストラクタを使ってゴールを証明する apply... with…
昨日のアレは、splitの定義があんまり一般的でなかったためのようだ。 変な定義でも証明が出来ることが分かったのでよしとする。 (* 私のやつ *) Fixpoint split' {X Y : Type} (l : list (X*Y)) : (list X) * (list Y) := match l with | [] => ([], []) | …
combine_splitが分からん。 証明は出来た。しかしどやってdestructを使うのか分からねえ。 Theorem split_fst_snd : forall (X Y: Type) ( l : list (X * Y)), split l = ((fst (split l)), (snd (split l))). Proof. intros. induction l as [| [x y] l']. …
オバマがシリア攻撃で議会に諮るということ自体が、すでにアメリカの威信が低下してることを示してんのかもしんない。 あのクリントンですら独断先行でスーダン爆撃を強行していたころに比べると。アメリカが無い世界とある世界の比較が出来ない以上、アメリ…
いまいっちょ集中出来ない。仕事そんなに忙しくないからよいものの。 喉が嗄れる。鼻がつまる。 今日のCoq 高階関数のところまで。javascriptや、schemeを齧ってると、すぐ出来る。 が型がある点がいままでとちょっと違う。 Foldで、f : X -> Y という関数を…
休日で、何もしない一日であった。知り合いが入院してたときに貸してたマンガが返ってきてしまったので、読み耽ってしまう。返さんでいいのに。 本日のCoq 型とか暗黙の引数とかイミフ。型ありの言語で、pairとlistは違うもんなんだなあ。ということを知る。…
ケンケン知らんの？と嫁に言われたが、知らんわ。 つーかワシの生まれる前のアニメのキャラかい。そっちが知ってるの方が変です。
半年くらい前から、少し歌うとすぐに喉が枯れるようになった。それで、喉が痛いと言って医者にかかったはずが、なぜか胃カメラを飲んでいた。 （逆流性食道炎の可能性ありとかなんとか） しかし喉も食道も胃も綺麗なもんだそうだ。 相変わらず喉は痛い。 今…
Coq modeで C-c C-f Find theorems containing: とミニバッファに出るので、定理を探したい型とか名前の一部とか入れると検索してくれる。Coqはまだ面白いけど、非形式証明になるとさっぱりお手上げ。 数学苦手。nとn'が同時に出てこられると混乱するんです…
$ cat << EOF > ~/.netrc machine github.com login yourname password **************** EOF $ chmod 600 ~/.netrc リストを使ったバッグにて。面白い定理とは何か？ 悪い意味で数学的になってるな。自分。
git の コメントをエディタ化$ git config --global core.editor vimcommitもaddもローカルでの変更リモートに反映させるには $ git push -u origin master
いやちょっと前から斜め読みしてたけど、限界が来たので、少し真面目に第一章からやる。http://proofcafe.org/sf/ https://github.com/moritanon/Coq_studygitも久しぶり触るのでなんもかんも忘れてる。仕事では使ってないし。 Theorem bin_nat_comm : foral…
