Coq Basics
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Install Coq
After installing coq, setup PATH variable point installed binaries (coqc, coqtop).
For example (macOS), if you installed coq from binary,
you will find the .app in your Applications directory:
/Applications/Coq-Platform~<version>~<month>.app/Contents/Resources/bin.
VsCoq Extension
Install VsCoq extension from marketplace.
Useful commands:
- About: explain the query.
- Check: check the type of query.
- Reset: Reset the focus to the start of the file.
- Interpret to End: Interpret to the end of the file.
- Interpret to Point: Interpret to the current point(cursor)
- Move cursor to the current focus(interpretation point)
- Step Forward: interpret next line.
- Step Backward: return to previous line.
Reference Manual
See official reference manual.