Coq theorem prover

First things first download and install coq. Information can be found here.

Installing Coqide has been pretty painless for me on ubuntu it is in the repositories, so I would go with that unless you are wedded to emacs, jrp recommended this website to get you started.

I am just a beginner so please correct any mistakes I make and take what I am saying with a healthy pinch of salt.

Basically there are two languages to coq that we will be investigating to start with, they are inter-twinned in the files.

One (Gallina) describes the mathematical structures and functions. It is somewhat similar to ML-ish functional programming languages.

The other is called the vernacular and deals with making proofs of certain statements. These statements can be used in further proofs. It involves rewriting and manipulating statements with tactics.

You use coqide to go through a file processing it bit by bit to find out where your errors are, and what happens when you apply certain tactics.