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
.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
,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
.