NII Shonan Summer School on Coq

K. Sakaguchi @pi8027

壁がほとんど全部ホワイトボードだけど、ホワイトボードマーカーが見当たらない。

Yoshihiro Imai @yoshihiro503

Lecture1 「Coqとは何か、なぜ使うか、どうやって使うか」 #CoqSchool

K. Sakaguchi @pi8027

今までずっと Eval compute in 書いてたけど Compute っていうコマンドがあったのか。

K. Sakaguchi @pi8027

Check, Print, Eval に並んで重要な Locate は出てこなかった。

Masaki Hara @qnighy

CompiteはEval vm_computeじゃなかったっけ　勘違いかな

Takashi Miyamoto @tmiya_

#CoqSchool 講師の講義内容に対して容赦なく他の講師から突っ込みが入っている…

K. Sakaguchi @pi8027

フランスでも Coq の同人誌が流行る！

K. Sakaguchi @pi8027

Coq'Art 持ってきてサイン貰えば良かったのでは……?

Takashi Miyamoto @tmiya_

#CoqSchool 午後の講座開始。

Takashi Miyamoto @tmiya_

#CoqSchool Check (@None bool). と書けば明示的に None の型を指定出来ます。

Takashi Miyamoto @tmiya_

#CoqSchool Print admin_person_ind. とか試すと、admin_person も inductive type であることが良く解る。

Yoshihiro Imai @yoshihiro503

#CoqSchool Record typesのコンストラクター like a mkAdmin は省略可能

Yoshihiro Imai @yoshihiro503

#CoqSchool admin_personのインスタンスは {| id_number := 1; ... |} みたいに書ける。

Yoshihiro Imai @yoshihiro503

#CoqSchool :: はリストのcons

Yoshihiro Imai @yoshihiro503

#CoqSchool ちなみにRequire Import Program すると、[1;2;3] のようなocaml風のリストnotationがavailableになる

K. Sakaguchi @pi8027

最終的に新刊だけでなく既刊も1部ずつプレゼントして、Yves Bertot さんにも1部ずつプレゼントして、なんか質問攻めに遭ってました。(英会話のできなさ……)

Yoshihiro Imai @yoshihiro503

#CoqSchool ohead関数の第一引数のカッコを丸かっこの代わりに{}を使って{A:Type}と書くと後でこの引数を省略して使える。

Takashi Miyamoto @tmiya_

#CoqSchool A が implicit になってるlistとなってないlistが混在してる？

Takashi Miyamoto @tmiya_

#CoqSchool Require Import List するとそこで定義されてるlistの定義では A はimplicit になるので省略出来る（推論してもらえる）

Yoshihiro Imai @yoshihiro503

#CoqSchool Fixpointコマンドは再起関数を定義するために使う。但し再起呼び出しの際に引数が構造的に小さくなっていなければならないという制限付き

Yoshihiro Imai @yoshihiro503

#CoqSchool myNatSの型は mynat -> mynat の間違い

k @mathink

Coq に関する講義なので(?) スライドの ``バグ'' もすぐに見つかる． #CoqSchool

Takashi Miyamoto @tmiya_

#CoqSchool のadvanced classで program semanticsの課題。解けるかなー。

Yoshihiro Imai @yoshihiro503

#Coqschool dinnerは19:00かららしい

Takashi Miyamoto @tmiya_

#CoqSchool ようやく bigstep_terminates が証明出来た。しかし今日は更なる強敵 terminates_bigstep が待ち構えている。