ProofCafe 第1回
ProofCafe 第一回でつぶやかれた内容です。おおまかな流れを実況したポストは、赤字にしてあります。
資料は、 http://coq.g.hatena.ne.jp/yoshihiro503/20100331 から辿れます。
by mzp2 fav 1368 view
まとめ
メニューを開く-
4人あつまってたけど、まだWindowsはあらわれていない #ProofCafe -
どえりゃーか、、流石に今日はust無い、、わな? #ProofCafe -
Mac 多し．できないことはないけど，まぁ，つぶやくという方向かと RT @r153: どえりゃーか、、流石に今日はust無い、、わな? #ProofCafe -
#ProofCafe 自己紹介タイム -
名刺持ってきたんで、あとで交換してください #ProofCafe
-
しまった名刺忘れた。 #ProofCafe -
対話環境はcoqtopです。あと拡張子は.vが一般的です。 #ProofCafe
-
式といってしまうと証明とかを全部含んでしまうので、いわゆるプログラムの式はGallinaといって区別します #ProofCafe
-
nat は自然数型 #ProofCafe
-
Gallina は 型も式である。 型の型は Set である。 だから たとえば「『nat型』の型」を調べる (Check nat.) と、 Set が返ってくる。 #ProofCafe
-
Set の型は Type. ではTypeの型は？ Typeの型はTypeなのである。 #ProofCafe
-
.@mzp の写真を見て、電源があることに気がついた。 #ProofCafe
-
#ProofCafe が終わるまで電池が持つかな？ -
ほかに 命題の型 Prop というのがある。 Check 1=2. と入力してみよう。 型 Propが返ってくる。 #ProofCafe
-
式を識別子に束縛するにはコマンドDefinition を使う。 識別子の名前は小文字でも大文字でもよい。 Gallina は 型も値と同様に扱えるので Definition t := list nat . のように型をDeifnitionで識別子に束縛できる #ProofCafe
-
Inductive コマンドで 型を定義する。 ここで Joker や Heart などはコンストラクタ #ProofCafe
-
Fixpoint は再起関数を定義する。 Definition との違いは、 定義本体で再起呼び出しができること。 #ProofCafe
-
Eval compute in fact 6. とかすると、factを評価できるよ。 #ProofCafe
-
Inductive は「帰納的」という意味。自然数のリストとかは Inductive nList : Set := | Nil : nList | Cons : nat -> nList -> nList. と帰納的なデータ構造 #ProofCafe -
Coq では、自然数は O (オー;ゼロの意味) と S n (n+1の意味)で表現する。 1, 2, 3.. などと書くと、自動的に S (S (S O)) などと 展開される。 #ProofCafe
-
match, with, end は予約語. #ProofCafe
-
match の end 必須なのは入れ子にしたときに嬉しい（OCaml 的な意味で #ProofCafe
-
Content from Twitter
コメント