Alperen Keles
Learner’s Guide to Coq Theorem Prover#1.
Posted on :: Tags: software engineering, algorithms, formal verification

Learner’s Guide to Coq Theorem Prover#1

Before I begin, I must state that I am pretty much not qualified to write about theorem proving in Coq, but that was pretty much the idea behind Learning From Learners, so I decided to try anyway.

https://xkcd.com/1856/

If you want a more comprehensive lecture style interactive book, go with a classic, Software Foundations ; if you wanna have your mind blown by dependent types, go with CPDT ; if you were as confused as I was when you hear about dependent types, I may be a good starting point to show you “How to Start Playing Around With Coq”.

So, what is Coq? According to Wikipedia :

“ Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification ”.

What is Coq? I hear you asking again. Simply put, it’s a programming system that allows you to prove your programs. You can write theorems about your code which then you can prove. It’s like testing, but without the testing part, and it actually works.

Let’s see the Hello World example for Coq.

Let’s break this down. bool is your old classic true and false . negb is “Negate-Bool”. negb_involutive is the interesting part.

\forall b: bool, negb(negb b) = b is our first theorem. We can actually easily check it for each both true and false to see that it is true.

b=true: negb(negb true) = negb false = true

b=false: negb(negb false) = negb true = false

In fact, the proof is exactly the same. Of course, to understand that, you need to understand what is going on.

When Coq sees the “Vernacular” Theorem , it expects a proof of the theorem after its definition. Proofs conventionally start with the Proof vernacular, denoting the beginning of the proof for documentation. The proof we see above is a sequence of “Tactics”, which are basically building blocks for your proof. They hide the complexity of Coq “Proof Terms”, and allow you to see your proof as a set of instructions.

Let me try to give a quick explanation of that paragraph.

A Coq program does not have a special proof mode. It is just a program. The difference is, it has dependent types. These are types that depend on values. They allow you to write your types as theorems. So, \forall b: bool, negb(negb b) = b is the type of negb_involutive . What do programs written in statically-typed languages do? They type-check.

So, when you have a definition that has a theorem as its type, you are supposed to write its proof, which would be the code that will allow the function to type-check correctly. It is not much different than the fact that we need a function returning integer to return an integer. (Kidding)

This phenomenon of “types are theorems, programs are proofs” arises from Curry-Howard Correspondence for anyone curious to go more into detail.

For the Javascript people, Tactics are like JSX elements hiding the HTML/CSS/Js behind.

A Vernacular is a top-level statement to tell Coq program is going to behave in a certain way. There are many different vernaculars, Inductive, Definition, Proof are three examples we have on the small piece of code.

Now, we can go inside the proof. 

Proof.
intros b. 
destruct b eqn:E.
- reflexivity.
- reflexivity.
Qed.
  • Proof is used to denote the start of sequence of tactics.
  • intros b turns \forall b into b in order to operate on the variable.
  • destruct b eqn:E is “Proof by Cases”. Remember, Inductive bool had two “constructors/members”, true and false . Hence, destructing b gives you two cases, b=true and b=false , we have now decided the value of the variable.
  • Each - allows us to focus on a single case, reflexivity just checks if two sides of the equality is “definitionally equal”. What definitional equality is a question I will not try to answer here.
  • Qed signals Coq that we have finished our proof, and we are ready for proof-checking. If proof-checking goes through, we start to https://tenor.com/bQ9Ws.gif ; else, we missed something in the proof.

As you see, there are lots of stuff going on the background, even the simplest example of a proof has to go through some complicated explanations. Yet, Coq is pretty good at abstracting many of these complications, as does all of our other programming systems.

I am thinking of moving on with these series with some follow-up articles. They will be much simplified/cut versions of Software Foundations, designed to mostly intrigue rather than teach. If this piece has attracted your interest in proved programming and Coq, please check the sources I leave below and let me know so I get motivated to write more about this.

Left(Le coq mécanisé taken from Ilya Sergey’s website, created by https://www.liliaanisimova.com/ ), Right(Coq logo from Twitter)