The Coq Proof Assistant

- Using Coq

- The Coq system, Windows version, is available for you to use in the SITE 0110 Computer Lab. You can run either Coq (which opens a Command Prompt Window) or CoqIDE (preferred). The class demo uses CoqIDE. Version 8.5 should be available on these machines by the start of the term.
- If you do not have an account which gives you access to the machines in the lab, you can get one. Click here for instructions. (If you are not an EECS student, you must be registered in the course to get an account.)
- You can get the Coq system here if you want to install it on your own computer.
- Propositional Logic in Coq

- Examples1.v: This file contains all the propositional examples covered during lectures, in a form that can be loaded directly into Coq.
- Predicate Logic in Coq

- Examples2.v: This file contains the predicate logic examples covered in class. They are in a form that can be loaded directly into Coq.
- protocol.v: This file contains part of the proof of the property of the SQR protocol covered in class. The rest of the proof is left as an exercise.
- Notes on Coq commands that correspond to natural deduction inference rules.
- The Coq tutorial is available in html, or pdf. Material to be covered in class includes Chapter 1, Sections 1.1, 1.2, and 1.3 on propositional logic, and Chapter 1, Section 1.4 on predicate logic.
- Further Coq documentation is also available online.
- Coq's main web page is here.
- Coq won the 2013 ACM System Software Award.