quartz-research-note/content/Coqの勉強.md

27 lines
1.7 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

#programming-language #memo #logic
[[Coq]]を用いた定理証明支援の基礎
- [Software Foundations 日本語訳](https://chiguri.info/sfja/)
- 大体これ読めばいいっぽい(プログラミング言語系は特に)
- 京都大学 [[五十嵐淳]] [「計算と論理」 授業資料(2023)](https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal/)
- 神戸大学 [Coq による定理証明入門 髙橋真(2023)](http://herb.h.kobe-u.ac.jp/coq/coq.pdf)
- 千葉大学大学院 [定理証明支援系 Coq での 論理的なリーゾニング 集中講義 アフェルト レナルド(2017)](https://staff.aist.go.jp/reynald.affeldt/coq/riron.pdf)
- IIJ技術研究所 [Coq を始めよう 池渕未来(2011)](https://www.iijlab.net/activities/programming-coq/coqt1.html)
- [Real World Coq An introduction to effective theorem proving](https://ejgallego.github.io/real-world-coq/) by [[Emilio Jesús Gallego Arias]]
- <https://x80.org/rwc/code/lesson_1.html> jsCoqを使ってインタラクティブに学べるDeepLとかのブラウザ拡張でレイアウトが崩れるっぽい
## 備忘録
- `Inductive`が変数宣言
- `Definition`が再帰しない関数宣言
- `Fixpoint`が再帰関数の宣言
- 再帰しないとwarningが出る
- 証明したい命題は`Goal`、`Theorem`、`Lemma`
- `Goal`は後で再利用されない、最後に証明したいもの
- `Theorem`と`Lemma`に違いはない
- こういうのめんどくさいな
- `Notation`って単純な文字列置き換えマクロとして実装されてるのかしら?
- Coqでは排中律が使えないので、ゴールの論理が論理和$A \cup B$とかの場合$A$か$B$のどちらかを証明するかを決めるしかない
-