2016-07-29

Software Foundations

仕事がつまらんので逃避中。

https://www.cis.upenn.edu/~bcpierce/sf/current/
読み始めて三年の月日が経とうというのに、まだ半分もいかない。
ちょっと読んでは分からんので中断し、忘れているので最初からやりなおしとかやってりゃ進まないのは当たり前。

というわけで三回目の挑戦中。
前半は大分書き変わってて、初版と比べて、だいぶ分かりやすくなった。と思う。(beautiful n とか、やはりいらない子だった。)
自分にとって、三回目だというのもあるかもしれないが。

前回、前々回と挫折したImp.vを今回初めて読了。数学力も数学学習歴ともに皆無のおっさんにはつらくて楽しい本だわいな。

Imp.vの中の問題やってる間、

forall X (l a:list X),  l = a ++ l -> a = [].

こんなの命題の証明があれば便利かな？とか思い証明しようとして、

Lemma app_any_is_nil : forall X (l a:list X),
  l = a ++ l -> a = [].
Proof.
(* lの帰納法で
  intros. induction l. apply app_nil_r in H. rewrite H. reflexivity.
  あれ？
*)
(* aの帰納法で。*)
  intros X l a. generalize dependent l.
induction a as [|xa a']. intros. reflexivity. intros. destruct l. inversion H. inversion H. Abort.

え？何で出来ひんの？。
まあ別に本編では結局いらなかったので放置してたけど、

さっき

Goal forall n a:nat,
       n = a + n -> a = 0.
Proof.
  intros. induction n.
  - rewrite  plus_0_r in H. rewrite H. reflexivity.
  - rewrite <- plus_n_Sm in H. inversion H. apply IHn in H1. apply H1.
Qed.

こんな感じで、リストじゃなくて自然数だったらすぐ証明出来るよなあ。とか考えてたら、lengthから証明すりゃいいのか。と思いついた。

Lemma app_any_is_nil : forall X (l a:list X),
  l = a ++ l -> a = [].
Proof.
  intros.
  assert(length l = length (a++l)).  apply f_equal. assumption.
  rewrite app_length in H0.
  assert(length a = 0).
  induction (length l).
  - rewrite plus_0_r in H0. rewrite H0. reflexivity.
  - rewrite <- plus_n_Sm in H0. inversion H0. apply IHn in H2. assumption.
  (* length a = 0 -> a = [] の証明 *)
  - destruct a.
   + reflexivity.
   + inversion H1.
Qed.

冷静に考えると小学生並のことしかやってないな。
でも、楽しいし、解けたら嬉しいのでよいことにする。一人初等数学。

2016-07-10

証明

この一週間くらい手を動かしてた、Software Foundationsの「サブシーケンスという関係は推移的である。」ということの証明が出来た!

めっさうれしい。

Inductive subseq : list nat -> list nat -> Prop :=
 | subseq_nil : subseq [] []
 | subseq_e : forall l1 l2 n, subseq l1 l2 -> subseq (n::l1) (n::l2)
 | subseq_ne : forall l1 l2 n, subseq l1 l2 -> subseq l1 (n::l2).

Theorem nil_is_subseq : 
  forall l, subseq [] l.
Proof.
  induction l. apply subseq_nil.
  apply subseq_ne. apply IHl.
Qed.

Theorem subseq_trans : forall l1 l2 l3,
  subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
  intros l1 l2 l3.
  generalize dependent l1.
  generalize dependent l2.
  induction l3 as [|x l3'].  
  - intros. inversion H.  apply subseq_nil. subst. inversion H0. destruct l2. destruct l1. apply subseq_nil. inversion H3. inversion H0.
  - intros.
    inversion H0 as [|l2' l3'' n|l2' l3'' n] .  subst.
    inversion H as [|l1' l2'' n'|l1' l2'' n']. subst. apply subseq_e. apply  IHl3' with (l2:=l2').
    apply H4. apply H3.
    subst.
    apply subseq_ne. apply IHl3' with (l2:=l2'). apply H4. apply H3.   
    subst. apply subseq_ne. apply IHl3' with (l2:=l2). apply H. apply H3.
Qed.

前に読んでよー分からんかった、inversionの動きがある程度分かった気がする。
コンストラクタの単射性ってなんやねんって感じだったけど、あるコンストラクタがある引数で作られる結果は唯一だから結果から逆算出来るということなのね。

2016-05-12

openssl

死ぬほど面倒くさい。
検証環境で中間証明書から発行されたオレオレサーバ証明書を作ろうとして嵌る。

テキトーにコマンドでオレオレ証明書発行して、nodejsのexpressサーバに中間証明書を設定すると、
chromeブラウザからの検証でエラーになって、強制的にページを見ることも叶わなくなる。

中間証明書はルート証明書と違い、以下の拡張要素が必要になるようだ。

[ v3_ca_middle ]
subjectKeyIdentifier=hash

authorityKeyIdentifier=keyid,issuer

basicConstraints = CA:true

フツーのエンド証明書と違い、(ルート証明書と同じく)basicConstrainsでCA:trueを設定しなくてはならないが、
ルート証明書と違い、(ユーザ証明書と同じく)authorityKeyIdentifierに、keyid,issuerを設定しなくてはならない。
(ルート証明書のauthorityKeyIdentifierは、keyid:always,issuer が設定されている。)

違いはよく分かってない。

でも確かに、むかーしRFCで読んだような気がしないでもない。

2016-01-05

clojure

clojureScriptを触るついでに。
clojureScriptはまださわれていない。

会社のproxy環境下でいろいろ動かなかった。
Light Tableでpluginの一覧が取れない。proxyパスワード存在下ではそもそもまだ動かないみたいだ。
leiningenはproxyパスワードに:が入ってたせいで動かなかった。
.splitしてんじゃねーよ。結局proxyのパスワードの方を変えた。

$ wget https://raw.githubusercontent.com/technomancy/leiningen/stable/bin/lein

$ lein repl

でインストールした上で、replが起動。初回は時間がかかる。

キーワードコロン":"から始まるやつ。rubyにあるシンボルと同じようなもん。
マップリテラル。jsのオブジェクトリテラルに相当。キーワードをキーにすると、キーワードが関数みたいにgetterとして使用できて便利

user=> (def m {:aaa 10})
#'user/a
user=>(:a a)
10

あと重複を許さないsetとか,lispらしく普通のlistとか。

>> という演算子で、xargsコマンドみたく実行を繋いでいける。

説明はここ
http://clojuredocs.org/clojure.core/-%3E%3E

演算子の記号をググれない問題。

letが普通のlispより括弧が少なくて済むとか言うけど、いくつか横に並べて書くと、どれか名前でどれが値だか分かんなくなるよね？

lisp系の言語のマクロだか関数だか区別がつかないの初心者を確実に遠ざけてるよな。

defmulti/defmethodは、いらんとまでは言わんけど、チュートリアルに載せるな。初心者が混乱するだけだと思う。

2015-12-13

scala

scalaコマンドによるreplとscalacコマンドでコンパイル出来るコードに違いがある？

Noneとかnil周りを自前で定義するような基本的なコードは、あまりreplで動かない？

Scala関数型デザインの本はあまりscalaコマンドぽちぽち叩く人向けではないのかもしれん。

replで通らないのは、こんなの。

package fpinscala.errorhandling

sealed trait Option[+A]
case class Some[+A](get :A) extends Option[A]
case object None extends Option[Nothing]


trait Option[+A] {
  def map[B](f: A => B) :Option[B] = {
    this match {
      case Some(a) => Some(f(a)) : Option[B]
      case _ => None
    }
  }
}

package文はreplでエラーになる。とどっかに書いてあったのでまあいい。
他はなあ。何が悪いのかエラーメッセージ見ても全く分からんわ。

<console>:21: error: constructor cannot be instantiated to expected type;
 found   : Some[A(in class Some)]
 required: Option[A(in trait Option)]
             case Some(a) => Some(f(a)) : Option[B]
                  ^

書き方がまずいらしいこと以外全く分からん。

2015-12-09

scala

Scala関数型デザイン&プログラミング―Scalazコントリビューターによる関数型徹底ガイド

作者: Paul Chiusano,Rúnar Bjarnason,株式会社クイープ
出版社/メーカー: インプレス
発売日: 2015/04/30
メディア: Kindle版
この商品を含むブログ (3件) を見る

この本が基本的なとこから説明してくれてて、とてもよさそう。
他の言語(boostやcoq)でも存在したoption型の何がすぐれているとか、ちゃんと書いてあるようだ。

これから読む。

2015-12-06

scala ブロック

どっかに

引数を一個だけ渡すメソッド呼出しでは、引数を囲む括弧を丸括弧から中括弧に変えてもよいことになっている。

とか書いてあった。

つまり、

println("hello world")

は、

println ｛ "hello world" ｝

と書いてもよい。と。
引数が関数リテラル一個であれば、なおさら、中括弧を使うべきなんだろう。実際そう書いてるソースが多い気もする。