途中ちょっとしたコードを保存するために、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…