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.

`.v`

.

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 → PWhat 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`

.