教科書系

Computation and Logic: Winter Semester 2021

Excerciseのやりかた

回答集
大学
Inductive Data Structures
ソース検索
GitHub - coq-community/coq-art: Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

Varnacular

Implicit Aruments

coq art 4.2.3.2
型推論できると省略できる。ただしArguments で{}で指定する。

tactics

rewrite nth occurence

coq - How to specify a location with the rewrite tactic? - Stack Overflow

at nはマッチした同一式で。もっと対象を絞るならその対象の式を与える感じ。

elim tactic

すぐ忘れます

coq - Elim versus induction - Stack Overflow
manicだからincudtionつかえとある。さよか。

http://pllab.is.ocha.ac.jp/coq/coq_print/nori_Coq4.pdf
Elilminationルールがあったとき、それを適用するんかいな
https://magicant.github.io/programmingmemo/coq/t-induct.html#elim
> 帰納的に定義された型を持つ項 term に対応する、帰納法を行うための関数を適用する。

asset tactic, cut tactic

assert vs cut
(使えるタクティク集)[https://www.iijlab.net/activities/programming-coq/coqt5.html]

auto系

jautoとかのほうがつよい。
(UseAuto_J: Coqの証明自動化の理論と実際)[http://proofcafe.org/sf/UseAuto_J.html]

|- *;みたいなのの謎

左が仮説、右がゴール。simplとかcbnとかrewriteの適用先らしいですね。なぞすぎた。わかった。

What is the meaning of "|-" in coq, and how do I find the definitions for the other seemingly undocumented notations? - Stack Overflow

Inductionを遅らせる

introsの前にってのがあった気がする。Coq art 13.11など。

仮説に関するInduction

Inclusion preserves well-founded
下記の導出に関する帰納法ってことか、、デジャブ

https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal21w/handout7.pdf

eilmとinduction

Coq タクティクリファレンス: 帰納法と場合分け
どっちか証明できて、どっちか証明できなくなるようなこたないのかい

split

introsと唯一のコンストラクタの適用とどこかに、、

absurd

なにやらtermと~termのゴールをつくる。coq artの回答に。。。
Coq タクティクリファレンス: 否定と矛盾

do, repeat

doは回数指定、repeatはできるだけ適用する

existsのelimination rules?case

caseするとforallになるとか。これはわからんな。と思ったら、constructorがでてくる。destructやelimはwitnessと仮説がでてくる。
https://magicant.github.io/programmingmemo/coq/byhyp.html

destruct

仮定の場合わけ。simple destruct 1は、、introsの連続とcaseらしい。なぜここでcaseか？
https://magicant.github.io/programmingmemo/coq/t-induct.html

misc

tupleで受ける

sigがtupleで受けられるらしい。なぞい。notationの話なのかな。
https://stackoverflow.com/questions/29591006/coq-program-matching-on-pair