xmldtp https://blog.hatena.ne.jp/xmldtp/ ウィリアムのいたずらの、まちあるき、たべあるきーPART2 https://xmldtp.hatenadiary.org/ Twitter 今日は、NII トップエスイー教育センターでCoqのお勉強。 その内容 その５ ■証明の仕方？（自分勝手にまとめたもの） ・まずは、intros forallに出てくる変数 ・simplする ・前に定義・証明したものを適用するには、rewrite その定義・証明 ・単純に同じものになったらreflexivity ■割とよく使うテクニック ・SearchPattern：指定の型 coqideの「Queries」→「Check」でチェック用のダイアログを出して、 SearchPatternでパターン検索できる。 ・SearchRewrite:等式に関する定理検索 coqideの「Queries」→… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fxmldtp.hatenadiary.org%2Fentry%2F28567de025d398cc11ea737f36af1019" title="Coqのお勉強　その５ - ウィリアムのいたずらの、まちあるき、たべあるきーPART2" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2011-07-12 16:24:31 rich https://xmldtp.hatenadiary.org/entry/28567de025d398cc11ea737f36af1019 1.0 100%