編集可能
2010年4月25日

ProofCafe 第1回

ProofCafe 第一回でつぶやかれた内容です。おおまかな流れを実況したポストは、赤字にしてあります。 資料は、 http://coq.g.hatena.ne.jp/yoshihiro503/20100331 から辿れます。
2
mzp @mzp

4人あつまってたけど、まだWindowsはあらわれていない #ProofCafe

2010-04-25 13:48:09
r153 @r153

どえりゃーか、、流石に今日はust無い、、わな? #ProofCafe

2010-04-25 14:10:19
クラなんとか @clairvy2

Mac 多し.できないことはないけど,まぁ,つぶやくという方向かと RT @r153: どえりゃーか、、流石に今日はust無い、、わな? #ProofCafe

2010-04-25 14:15:49
mzp @mzp

名刺持ってきたんで、あとで交換してください #ProofCafe

2010-04-25 14:11:57
mzp @mzp

対話環境はcoqtopです。あと拡張子は.vが一般的です。 #ProofCafe

2010-04-25 14:13:14
mzp @mzp

式といってしまうと証明とかを全部含んでしまうので、いわゆるプログラムの式はGallinaといって区別します #ProofCafe

2010-04-25 14:18:06
Keigo Imai @keigoi

Gallina は 型も式である。 型の型は Set である。 だから たとえば「『nat型』の型」を調べる (Check nat.) と、 Set が返ってくる。 #ProofCafe

2010-04-25 14:21:21
Keigo Imai @keigoi

Set の型は Type. ではTypeの型は? Typeの型はTypeなのである。 #ProofCafe

2010-04-25 14:21:21
shimomura @shimomura1004

.@mzp の写真を見て、電源があることに気がついた。 #ProofCafe

2010-04-25 14:22:24
Daisuke NISHITANI @cho_tekitou

#ProofCafe が終わるまで電池が持つかな?

2010-04-25 14:22:29
Keigo Imai @keigoi

ほかに 命題の型 Prop というのがある。 Check 1=2. と入力してみよう。 型 Propが返ってくる。 #ProofCafe

2010-04-25 14:24:14
Keigo Imai @keigoi

式を識別子に束縛するにはコマンドDefinition を使う。 識別子の名前は小文字でも大文字でもよい。 Gallina は 型も値と同様に扱えるので Definition t := list nat . のように型をDeifnitionで識別子に束縛できる #ProofCafe

2010-04-25 14:25:49
Keigo Imai @keigoi

Inductive コマンドで 型を定義する。 ここで Joker や Heart などはコンストラクタ #ProofCafe

2010-04-25 14:26:39
Keigo Imai @keigoi

Fixpoint は再起関数を定義する。 Definition との違いは、 定義本体で再起呼び出しができること。 #ProofCafe

2010-04-25 14:28:13
mzp @mzp

Eval compute in fact 6. とかすると、factを評価できるよ。 #ProofCafe

2010-04-25 14:27:30
でこれき @dico_leque

Inductive は「帰納的」という意味。自然数のリストとかは Inductive nList : Set := | Nil : nList | Cons : nat -> nList -> nList. と帰納的なデータ構造 #ProofCafe

2010-04-25 14:28:40
Keigo Imai @keigoi

Coq では、自然数は O (オー;ゼロの意味) と S n (n+1の意味)で表現する。 1, 2, 3.. などと書くと、自動的に S (S (S O)) などと 展開される。 #ProofCafe

2010-04-25 14:29:46
でこれき @dico_leque

match の end 必須なのは入れ子にしたときに嬉しい(OCaml 的な意味で #ProofCafe

2010-04-25 14:31:18
残りを読む(51)

コメント

mzp @mzp 2010年4月25日
第一回のProofCafeでつぶやかれた内容のまとめです。 yosihiro503の話した内容を実況しているポストは赤字にしてあります。 http://coq.g.hatena.ne.jp/yoshihiro503/20100331
0