Coqのお勉強 その５

今日は、NII　トップエスイー教育センターでCoqのお勉強。

その内容　その５

---

■証明の仕方？（自分勝手にまとめたもの）

・まずは、intros 
　　　forallに出てくる変数
・simplする
・前に定義・証明したものを適用するには、rewrite その定義・証明
・単純に同じものになったらreflexivity



■割とよく使うテクニック
・SearchPattern：指定の型
   coqideの「Queries」→「Check」でチェック用のダイアログを出して、
   SearchPatternでパターン検索できる。

・SearchRewrite:等式に関する定理検索
   coqideの「Queries」→「Check」でチェック用のダイアログを出して行う

・標準ライブラリ
   http://coq.inria.fr/stdlib/
   Arithなど

・locate "記号"　：　記号に関するものを検索
 　locate "+" など
   coqideの「Queries」→「Check」でチェック用のダイアログを出して行う

・関数の定義を展開するunfold（逆はfold)

・再帰関数
　Functionコマンドを使う
　　　→Fixpointで定義できないようなもの
　Recdefをインポートすること
　measure length xsなどmasureを入れる