今日のCoq

仕事が一区切りついてなりより。まあ9月から相当手抜いてました。すいません。
次の仕事の話を聞いてきたけど、かなり地雷臭いな。

---

なんとかProp_J.vを追加練習問題除いて終了。
Logic_J.vに入った。あいかわらず証明オブジェクト書くところで超モヤモヤしてたんだけど、Coqで何が分かってないかやっと分かった気がする。
関数の適用が左結合、（って言うので合ってるかしら）であること。

    Inductive ev : nat → Prop :=
       | ev_0 : ev O
       | ev_SS : ∀ n:nat, ev n → ev (S (S n)).

という命題定義において、

「ev 4.」という命題の証明オブジェクトは以下の形になる。

ev_SS 2 (ev_SS 0 ev_0).

ここで冒頭二単語取り出して型を見てみる。

Check ev_SS 2.

すると、

ev_SS 2
     : ev 2 -> ev 4

となる。
これは、
「ev 2」という命題(型)を引数に取って、「ev 4」という命題（型）を返却する関数である。
その関数が、 (ev_SS 0 ev_0).という命題を引数に取る。

この引数がどないなっているかとちうと、

ev_SS 0 は、 「ev 0」という命題を引数に取って 「ev 2」という命題を返す関数であり、「ev 0」という命題は、 ev_0 というコンストラクタが生んでくれる。（すなわちそれが究極の根拠になる）

そして、昨日読んだように、

A→B という型も ∀ x:A, B という型も、どちらも型 A から型 B への関数である、という点については同じです。

であり、今日 Logic_J.vに書いてあったように、

実は、→ と ∀ は 同じものです! Coqの → 記法は ∀ の 短縮記法に過ぎません。仮定に名前をつけることができることから、 ∀記法の方が一般的です。 
・・・

これはつまり "P → Q" は単に "∀ (_:P), Q" の糖衣構文に過ぎないと いうことを示しています。 

なのである。

letがlambda の糖衣構文であるって読んだときのような衝撃!
当時はお前は何を言ってるんだ。もっと分かりやすく言ってくれよ。という感じであったが。

---

最新のソフトウェアの基礎の原文を訳そうかと。差分訳すだけだしなんとかなんじゃね。とsfjaのforkを行なってみた。

が、序章からして結構違うのね・・・