The Coq proof assistant

I must admit that I really like the Coq - it's terrific tool that already feels rather nice even though I haven't got much experience with it. It can be used as a proof assistant in proving theorems in Calculus of inductive constructions and as a tool for building verified programs. I plan to explore its reach more completely in later posts after I've played with it more.

Here's example from the Coq's standard library:

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Definition pred (n:nat) : nat := match n with
| O => 0
| S u => u
end.

Theorem pred_Sn : forall n:nat, n = pred (S n).
Proof.
simpl; reflexivity.
Qed.


This is pretty much normal way to define natural numbers as zero and its successors. In coq this means that we are defining this type called nat that nat is either O or successor of a nat. Inductive in the beginning means that this definition declares way to construct instances of this type - which in turn means that coq will produce nat_ind, nat_rec and nat_rect - way to do inductive statements and recursive operations on nats. Definition of predecessor function is very straightforward and theorem of every natural number being predecessor if its successor is also easy to read even if one might not know what simpl and reflexivity are - they are called tactics and proofs in coq are build from them.

The Coq tutorial was rather nice introduction if rather short and now my prime source of information about the Coq are its reference manual and standard library - both of which are rather readable and intresting even though I have just started learning coq. Other people have written about it much more elegantly, but since this is learning experience it doesn't really matter.

I must admit that the french can name things well - I mean what would be better name for a tool?