Imp.v 初めて読むところが多くなってきたので読むスピードが落ちる。 スピードが0になったら終わり。一度手動で全部書いてからでないと、「便利なタクティカル」とやらをちっともどうやって使ったらいいのか分からない。いずれ慣れるのだろうか。プログラミ…

Software Foundations Imp.v 全開前回挫折したとこまで再び到達。前よりは若干分かってる感じもする。http://d.hatena.ne.jp/morita_non/20130928/1380366939 で書いた、関係 bevalR のどこが間違ってるとか。関係なのに、関数aevalと混ぜたらあかんやろ。 R…

MoreInd.v 帰納法のための明示的な証明オブジェクト を読む。目的の集合を数え上げ尽すことが出来れば、コンストラクタは何でもよい。という意味だと理解。そういうわけで、以前の l=rev l -> pal l も、 list Xのコンストラクタを変えて、新たな帰納法の原…

PHPについて少し調べてる。次の仕事がそれだし。 何か作るのがいいんだろうけど、何か作りあげるような根性とか意欲はもちろんない。pukiwikiって現在のPHP5.x系で動かないんだね。あれ結構使ったのに。直系のアプリもなさそう。みんなWiki記法なんてものは…

ついったで(Coq方面の)その筋の人らをフォローしてると、たまに「面白い証明を求む」とか、それくらいの証明じゃ面白くないとか、そういう呟きが流れてくることがある。しかし、面白い証明っていったい何なの？ 難しかったり、アクロバティックだったりする…

ProofObject.v これこそが知りたかったことだけど、すでに前の版で大半は日本語訳されてた。例とかは少ないけど。 以前読んだときは目に入ってなかったのか、理解出来てなかっただけか、両方か。しかし、Printとかの使い方はなかった気もする。 Theorem b_ti…

MoreLogic.v 練習問題。all_forallbようやっと、Coqで仕様を記述し、証明する。という本来の目的のモノが出てくる。問題は、「仕様とは何か？」ということが分かってないことだが。とりあえず、allを以下のように書く。これはこれで間違ってはいない・・・と…

Rel.v 反射推移閉包とかこれ何かの役に立つんじゃろか。関係をラップするとか。clos_refl_transとかrefl_step_closureとかまったく意図とか分かってないけど、だいたいこんな感じだろうというレバガチャで証明は出来た。何の役に立つとか、読み進めたら出て…

Prop.v *** Exercise: 3 stars, optional (R_fact) にて、That is, if R m n o is true,って書いてあるけど、R m n oは命題なんだから、Trueじゃね？と思う。 でもSoftwareFoundations/coqの世界のなかで、Trueとは、 True : Prop := I : True.でしかないか…

Software Foundations Rel.vより Definition partial_function {X: Type} (R: relation X) := forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2. Theorem le_not_a_partial_function : ~ (partial_function le). Proof. unfold not. unfold partial_functio…

途中ちょっとしたコードを保存するために、gistを使ってみた。 わりいいけど、大きなファイルを何度も書き換えたりする用途には、githubでリポジトリにファイル置くのがよいっぽい。

Software Foundationsを読んでると、時々、「なんか自明でない定理考えて証明しろ」とか無茶振りしてくるけど、数学に慣れてない人間にんなこと言われても途方に暮れるわけだ。そもそも、何か命題があって、それを証明する必要があるかどうか、ということが…

Inductive 型とか命題の定義を行う。 回文の定義で、 Inductive pal {X:TYpe} : list X -> Prop := | p_zero: pal [] | p_one : forall x:X, pal [x] | p_2 : forall l, pal (l ++ (rev l)) | p_3 : forall l1 l2, pal l2 -> pal (l1 ++ l2 ++ (rev l1)).と…

Software Foundation Prop.v forall l, l = rev l -> pal l.どっから手をつけたらいいかすら分からん・・・前問の forall l, pal l -> l = rev l.ならば、"pal l"という命題を定義してあるから、そのコンストラクタに応じて場合わけして、それぞれが l = rev…

Logic.v 証明オブジェクトがどんなかたちになるかについて、 全然イメージが湧かない。 あいかわらずレバガチャ状態ではある。 Theorem or_distributes_over_and_2 : forall P Q R : Prop, (P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R).とか。scriptモードでも、…

どれが型で、値で、という区別。 どれが命題で、証明で、という区別。 慣れるしかないとはいえつらい。しばしば出て来る数学用語についても、もう少し知っておく必要がある。直積、関係、反射的、推移的、対称的、etc...学がないとつらいね。SoftwareFoundat…

Logic.v証明オブジェクトが良くわからん。論理積の交換で、Logic.vに載ってるやり方だと以下のような証明オブジェクトが作られる。 Theorem and_commut : forall P Q : Prop, P /\ Q -> Q /\ P. Proof. intros P Q H. inversion H. split. apply H1. apply H…

型推論は、型を推論するものである。多相的な型の型パラメータの値は、推論される型じゃないので省略出来ない。 Inductive list (X:Type) : Type := | nil : list X | cons : X -> list X -> list X.の Xみたいなやつね。型パラメータを持つ多相的な型のコン…

Lists.v 自分で問題を考えましょう。 - [cons] （[::]）、 [snoc]、 [append] （[++]） に関する、自明でない定理を考えて書きなさい。 とかいう問題が一番なにしたらいいか分からない。 定理ってどうやって思い付けばいいの？ Lemma nil_rev : forall l : n…

関数を宣言するときに型パラメータを暗黙に指定させてしまうことも出来るようだ。 Fixpoint length {X:Type} (l:list X) : nat := match l with | nil => 0 | cons h t => S (length'' t) end.{X:Type}のように中括弧で宣言すると型パラメータは実際に書かな…

再読中。 ここをあーはいはいリストね。ペアね。ってな感じで流し読みしたことが あとでつまった原因の一つだと思われる。出来ない人間が挫折する理由は無限にあるし、教育者ってたいへんだなと思う。 まあ出来ないやつはほっとかれるだけであろうが。

二進数のnormalizeに関して、normalizeした二進数が必ずnormalizeする前のものより短くなることを証明してみた。 証明することは出来たが、命題に対する帰納法ってやつをあんまり理解していないことが分かった。(最初、n S n 帰納法でやってしまって泥沼に嵌…

coqのワイルドカードって、データしかあかんのか？ Fixpoint bin_len (b : bin) : nat := match b with | Q => O | T b' => S (bin_len b') | F b' => S (bin_len b') end.を Fixpoint bin_len (b : bin) : nat := match b with | Q => O | _ b' => S (bin_l…

http://d.hatena.ne.jp/propella/20090215/p1 Coq < Parameter a b :nat. a is assumed b is assumed Coq < Print plus. plus = fix plus (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus p m) end : nat -> nat -> nat Argument s…

SF Induction.v #coqnormalizeにて、Prove It. とだけ書いてあるんですが、何を証明すればよいのでしょうか。これ？ 取り敢えず、normalizeする前の二進数とした後の二進数で、同じ自然数に変換出来ることは証明したけど、 これって意味あるんだろうか？そも…

Coqコマンドの Print/Locateを教えてもらった。 チュートリアルの一番最初にのっけておいて欲しかった。途中で挫折して読めてない後ろの方に載ってんのかもしらんが。 Check 式の型を表示。 Print 関数や型の定義を表示。 Locate Notation を展開して表示。N…

オンライン演習も終ったし、仕事がヒマな内に、Coqに戻るかと思ったけど、やはりもう色々忘れてていろいろいやになる。年とるのってやだねえ。しかし若いころは経験と理解力と忍耐力が足らんかったから余り変わってないかもしれん。 Software Foundation Bas…

最近あらゆる義務を放棄してこればっかりやってたけど、おわた。 残念だ。あと100問くらいあってもいいのに。 こんなに熱中したのは10年くらい前のガンパレ以来かもしらんやはり、再代入はプログラミングにおいて必要かもしらんが、悪であると断言する。 参…

137問まで来た。 http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/index.cgi?command=stats のページを見てニヨニヨするのがここ最近の楽しみだったんだけども。最近はあまり順位が変動しなくて寂しい。何問も解かないと順位があがらないし。佐野さんとい…

「別に「副作用」の発生が悪い，というわけではなく，単に，主たる効果が，値の計算・実行の終了であるとした時には，そう呼べる，といういわば相対的な概念である．現実世界で意味のあるプログラムの動作のほとんどは副作用である，という見方も可能である」