Type Theory at SSFT - slides and exercises - Level 0

This lecture is 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

a script language to efficiently interact with Coq
a range of mathematics already developed in Coq, in the form of mathematical libraries.

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

Installation

Here is a page that will give you instructions for installing Coq (>= 8.7) 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

helloworld
	: P → P

What happened there?

Require Import ssreflect loads Ssreflect.
Variable P:Prop declares a proposition P. The fact that P stands for a proposition is indicated by the type annotation :Prop (similar to Caml's type annotations).
Theorem helloworld: P -> P ,
tells Coq that you want to prove a theorem whose proof will be called helloworld, and whose statement is P -> P, where the symbol -> stands for implication. Once Coq understands this, it switches to the proof-editing mode, indicating in the side window the (sub)goal that you have to prove.
Proof does nothing but remind you that you are now in proof-editing mode.
done asks Coq to finish the proof without further intervention on your part. Luckily in this (very simple) case, Coq finds a proof and returns that the proof is completed.
Qed exits the editing of the proof, binding it to the name helloworld.
Check helloworld asks Coq if it knows of something called helloworld, and Coq replies that it is indeed a proof of P → P.