ProofCafe 第1回
ProofCafe 第一回でつぶやかれた内容です。おおまかな流れを実況したポストは、赤字にしてあります。
資料は、 http://coq.g.hatena.ne.jp/yoshihiro503/20100331 から辿れます。
-
- いいね！0
Keigo Imai
@keigoi
@osiire いわゆる induction principle です。 構造帰納法を使った証明のために必要です #ProofCafe
2010-04-25 14:31:49
Keigo Imai
@keigoi
rlwrap coqtop で coqtop 中でも readline 環境になって 幸せになれます。 #ProofCafe
2010-04-25 14:36:55
でこれき
@dico_leque
トップレベルの言語が Vernacular で計算とかを書く言語が Gallina。 Fixpoint とかの大文字で始まるのが Vernacular、 match 〜 with 〜 end は Gallina の予約語 #ProofCafe
2010-04-25 14:37:36
Keigo Imai
@keigoi
intro h は、ゴール (====の下) が P -> Q (PならばQ) の形 のとき Pを仮定に追加 (====の上に移動) して、残ったゴール Q の証明に移る。 #ProofCafe
2010-04-25 14:40:55
Keigo Imai
@keigoi
Restart. で証明を最初からやりなおし。 Undo. は 直前の Vernacular コマンドを取り消す。 Undo n. でコマンドを n個取り消す。 #ProofCafe
2010-04-25 14:47:08
Yoshihiro Imai
@yoshihiro503
#ProofCafe #ProofGeneralのコマンド集 http://www.itpl.co.jp/ocaml-nagoya/index.php?ProofCafe%2FProofGeneral
2010-04-25 14:53:14
Keigo Imai
@keigoi
あー途切れていた。 induction xs. で xs に関する帰納法が始まる。 xs が nil のときと cons の時の場合分けになる。 どちらの場合も まずは simpl. で式を簡約する。 #ProofCafe
2010-04-25 15:03:30
Keigo Imai
@keigoi
xs=nil のとき、 = の両辺は 構文的に等価になる。 このとき reflexivity 炊くティックで証明を完了できる。 #ProofCafe
2010-04-25 15:04:12