Coq for SSFT'2018 - Type Theory exercises - Level 0

This course is very connected to a 9-week course on Computational Logic given at École Polytechnique in France.

Coq is a proof assistant, a.k.a. interactive theorem prover: it helps you prove theorems, interactively.
Interaction means you send Coq some commands, you get back some answers.

Developing proofs in a proof assistant is "like" developing code in a programming language, inasmuch we will use en environment called Proof General to develop proofs in Coq, just like you are used to Eclipse to develop code in Java. Proof General is based on the Emacs text editor.

Moreover, we will use an extension of Coq called Ssreflect (Small Scale Reflection) that provides

Coq's "source files" have the extension .v.


Hopefully, Coq should be installed on your SSFT Virtual Machine, with version >= 8.7. If it is not (or if the version is older), here is a page that will give you instructions for installing Coq directly in your OS or in the SSFT Virtual Machine (which is a Linux machine).

Hello world

Open the file helloworld.v in Proof General.
Commands in Coq finish with a full stop.

Find the button/key that sends the next command to Coq. By using it several times, you should sequentially get the following answers:

P is declared
1 subgoal
P → P
No more subgoals.
helloworld is defined
	: P → P
What happened there?