Coq and Gallina

No, I haven’t suddenly picked up raising hens as a hobby, but Coq in this case is interactive proof assistant that I have been trying to learn to use during my summer vacation.

Coq is an interactive proof assistant that can be used to construct and prove theorems. For example, to prove that zero plus any natural number is equal to that same natural number, one could write proof as:

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. 
  simpl. reflexivity.
Qed.

While such a proof isn’t particularly exciting, it’s a start as one can reuse theorems to proove more complex theorems. I’m using Software Foundations as reading material and so far I have been happy about it. Of course working alone without teacher is somewhat slower than if I were in university class.

So, why I’m playing with theorems and proofs? It’s possible to write programs using Gallina (the programming language that Coq uses) and then prove some mathematical property about it. If I were to write a function that appends an element to a list, I could prove that the resulting list contains the appended element in addition to all the elements that already were there. Again, super simple (from the point of view of the functionality), but these small functions can be used to build more complex programs. And more complex programs can be proven to have some mathematical properties.

Things get really interesting when you consider the fact that one can export programs written in Gallina to some other language, which in my case most likely would be Haskell. This would allow me to write core functionality of a program in Gallina, prove mathematically that it actually does what I want it to do and then export it into Haskell. And then add rest of the things in Haskell that I couldn’t write in Gallina.

So if unit tests are used to show that function does what is expected with some specific values and property based tests can show that some property holds with some amount of randomly generated values, mathematical proof can show that function works as intended with every value. Which is still different from software doing what user expects it to do (the theorem might be incorrectly stated or person writing software misunderstood what it was expected to do).

All this is very much theory at the moment as I’m working my way through the basics of Coq and Gallina. The most recent theorem I was able to prove was following:

Theorem eqb_true : forall n m,
    n =? m = true -> n = m.

Which pretty much states that if equality comparison between n and m returns true, n and m are equal. So nothing fancy and very much very far away from any useful program.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s