Coq (Art)のわからないメモ
教科書系
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
いいなと思ったら応援しよう！
