How to write correct code by construction using the Coq Proof Assistant

Paul Cadman and Walter Schulze playing with wooden blocks in preparation for the talk

Software can be incredibly buggy. Look at all these errors:

There are many cases where these bugs have consequences beyond throwing your phone at the wall:

Where do we ask for help when Stack Overflow or ChatGPT is down?

People call us developers, architects, or even worse, engineers — as if we are calculating structural integrity before we start building. We are just playing with wooden blocks, and suddenly someone walks in the room, very impressed, and asks us if our miniature village can scale to real humans living in it. Like an enthusiastic five-year-old, we say yes. We want humans living in woodblock villages without any nails or cement. We think this is realistic. They should call us Software Toddlers, not Software Engineers.

Software Toddlers. Image Credit: Jeroen Kransen

It is probably a good idea to verify the most important parts of your code, as all of these products have done:

The WebAssembly specification has been formalised using Isabelle
Important parts of TLS that are used in Chrome and Firefox have been verified using Coq
Smart Contract languages like Zilliqa’s Scilla
Blockchain protocols like Tezos
Cosette, a SQL Optimizer
Rustbelt can be used to prove the unsafe parts of Rust code are safe

These projects use mathematical proofs that are verified by the computer. We call these verification programs, Proof Assistants. Now just to warn you, you might not understand everything in this article, and that is okay. The main takeaway is that there are tools to do more rigorous programming with and to give you a little demo of what it is like using them.

If you prefer, you can watch the talk below, which covers the same material as this post.

Binary Search Tree in Kotlin

As an example, we will look at how to verify a Binary Search Tree, a popular topic for coding interviews.

In a Binary Search Tree, the values are stored in the tree so that all left children are less than their parents and ancestors, while all right children are more than their parents and ancestors. This way, it is possible to search through the tree in O(log(n)) time and insert the tree in O(log(n)) time as well, which is an efficient solution for some use cases.

Binary Search Tree

We will code up the Binary Search Tree in Kotlin to use some syntax lots of people are used to. We use a sealed class, which means it can be constructed in two ways:

a Nil tree, which has no children
a Node with a value and two children called lefty and righty

sealed class Tree {
  object Nil : Tree()
  data class Node(
    val lefty: Tree,
    val value: Int,
    val righty: Tree
  ) : Tree()
}

The contains function for a binary search tree can be written with pattern matching. Recursing down the left or right, depending on what is appropriate according to the properties of the Binary Search Tree. Here’s the code:

fun Tree.contains(x: Int): Boolean=
  when (this) {
    Tree.Nil -> false
    is Tree.Node ->
      if (x          lefty.contains(x)
      } else if (value          righty.contains(x)
      } else {
         x==value
      }
  }

We can make sure this is correct using Unit Tests like the following:

@Test
fun `tree with a single node 1 contains 1`() {
    val tree=Tree.Node(Tree.Nil, 1, Tree.Nil)
    assertThat(
        tree.contains(1)
    ).isTrue()
}

If you are lazy, like me, and don’t want to think of all cases, you can use a property-based test. This randomly generates the inputs and makes sure that whatever is inserted into the tree is contained in it after I insert it.

@Property
fun `inserted value is contained in tree`(
    @ForAll("trees") tree: Tree,
    @ForAll ivalue: Int
) {
    assertThat(
        tree.insert(ivalue)
            .contains(ivalue)
    ).isTrue()
}

These properties look mathematical and are actually something we could prove in Coq. This would even catch the recursive edge cases that could be missed. Also, the tests won’t take forever to run and clog up your CI since it will be checked at compile time.

A First Proof Using a Construction Toolbox

Let’s start with a basic proof of comparisons, which we’ll also need to use later. We want to prove that for any two natural numbers x and y, if x then x . This is not true in the reverse, but if one number is less than another, then that means that the number is less than or equal to the other number.

__________________________________
forall (x: nat) (y: nat),
  (x

This is the proof state. What we need to prove is below the line, and any hypothesis we have to complete the proof is above the line.

At the moment, we have nothing above the line, but we can nail some things to the wall using a hammer.

x: nat
y: nat
H: x __________________________________
x ≤ y=true.

Now, we only need to prove the comparison below the line. Everything above the line is now a given or assumption. We can also introduce other tools from our toolbox or previously proven theorems. For example, we have already proven that if x then x and x is not equal to y. We introduce this tool above the line.

Tool: (x x: nat
y: nat
H: x __________________________________
x ≤ y=true.

Note: The / operator represents “and,” which is also called conjunction.

We can now apply the Tool like we would apply a function. We can use H as a parameter to the Tool and get a new hypothesis called Tool H.

- Tool: (x + ToolH: (x ≤ y=true) / (x==y=false)
x: nat
y: nat
H: x __________________________________
x ≤ y=true.

Note: the Diff syntax is used to show which hypotheses were removed and added compared to the old state of the proof.

Now, we need to break up the conjunction in ToolH into its two separate parts. We can call our friend Wreck-It Ralph to help us. He is also in construction.

Wreck-It Ralph

- ToolH: (x ≤ y=true) / (x==y=false)
+ Leq: x ≤ y=true
+ Neq: x==y=false
x: nat
y: nat
H: x __________________________________
x ≤ y=true.

Now the goal we want as a hypothesis is above the line, which means what we want to prove is a known fact. This means we have completed our proof. We say “Qed,” which means that the proof is complete.

Coq Proof Assistant

Buy high-vis jackets for your own chickens: https://www.omlet.co.uk/shop/chicken_keeping/high_vis_chicken_jacket/

Now that we have completed a proof, we can try doing one using a Proof Assistant called Coq. Coq is a Proof Assistant because it not only keeps track of our proof state but can also check if our proof is correct and helps us search for tools to apply. Here is our proof from before, written in VS Code using the VSCoq plugin.

This allows you to type the tools you want to use on the left, and the proof assistant will provide hints on the right. The hints include the hypotheses available to us to use above the line and the goal we need to prove below the line. On the left, we can type our proof and evaluate or check it as we go. The right will reflect the current state of the proof and include all the hints we have accumulated in the green parts of the code. We can then step up and down to change the hints provided on the right by the assistant.

First Proof in Coq

We need to prove that if x then the following is not true y . This is a theorem that we will need later to prove our BST implementation is correct. We write this theorem in Coq:

Theorem Lt_implies_not_Lt:
  forall {x: nat} {y: nat},
  (x   -> y Proof.

This results in the following proof state:

--------------------------------
forall x y : nat, (x  (y

The first thing we want to do is use our hammer and nail some things to the wall, using nail:

x, y: nat
H: (x --------------------------------
(y

Next, we can explore all cases of the comparison using compare x y as C. This results in three cases for C: x=y, (x and (y . We have to prove for each of these three cases that (y .

x, y: nat
H: (x C: x=y
--------------------------------
1/3
(y --------------------------------
2/3
(y --------------------------------
3/3
(y

We can focus on a single goal using a dash - character:

Theorem Lt_implies_not_Lt:
  forall {x: nat} {y: nat},
  (x   -> y Proof.
nail.
compare x y as C.
-

This allows us to first focus on the case where C is x=y:

x, y: nat
H: (x C: x=y
--------------------------------
(y

We can see that the fact that x=y has already been used to rewrite the goal and replace x with y. This was done by the compare tool for us.

We can use Coq to search for a theorem that can help us with our proof using SearchRewrite (?X , which finds the theorem Nat.ltb_irrefl: forall x : nat, (x . We can use this theorem and substitute (y , with false using sub Nat.ltb_irrefl.

Nat.ltb_irrefl: forall x : nat, (x x, y: nat
H: (x C: x=y
--------------------------------
- (y + false=false

Note: the Diff syntax used to show the old goal as removed and the new goal as added.

The left and right side of the equality is the same, so we can simply tell Coq this using the tool same to finish the proof of the subgoal. We can now focus on the second subgoal:

x, y: nat
H: (x C: (x --------------------------------
(y

If we have a goal B and a theorem that A implies B, it means that if we prove A we have proven B. It is like applying the function A -> B in reverse. Another theorem that someone else has already proven is available ltb_ge: (x (y . We can use the apply ltb_ge tool to update the goal since the goal is the same as the return of this theorem.

ltb_ge: (x  (y x, y: nat
H: (x C: (x --------------------------------
- (y + (x

Now, we can apply the theorem we proved before Lt_implies_Leq: forall (x: nat) (y: nat), (x . Again, we can apply this in reverse using apply Lt_implies_Leq.

Lt_implies_Leq: forall {x: nat} {y: nat},  (x x, y: nat
H: (x C: (x --------------------------------
- (x + (x

Note: the curly braces say that the parameters are implicit and can be inferred without us explicitly passing them.

The goal is now exactly the same as two of the hypotheses, so we can finish this subgoal using just Hand start to focus on our final subgoal. This final subgoal could be more interesting since it is proven in the same way as the previous subgoal.

apply ltb_ge.
apply Lt_implies_Leq.
just H.

This means we have completed our first proof in Coq:

Require Import ConstructionToolbox.Theorem Lt_implies_not_Lt:
  forall {x: nat} {y: nat},
  (x   -> y Proof.
nail.
compare x y as C.
- SearchRewrite (?X   sub Nat.ltb_irrefl.
  same.
- apply ltb_ge.
  apply Lt_implies_Leq.
  just H.
- apply ltb_ge.
  apply Lt_implies_Leq.
  just H.
Qed.

We use Qed to indicate the proof is complete. The Coq compiler will check that this proof is correct and all subgoals have been completed. Otherwise, we will get a compiler error.

Coding in Coq

We just wrote a proof in Coq, but we can also write code. Here we have the tree I wrote in Kotlin:

sealed class Tree {
  object Nil : Tree() {}
  data class Node(
    val lefty: Tree=Nil,
    val value: Int,
    val righty: Tree=Nil
  ) : Tree()
}

Here is the same Tree structure defined in Coq:

Inductive tree: Type :=
  | Nil
  | Node
      (lefty: tree)
      (value: nat)
      (righty: tree).

It also has two constructors:

a Nil tree, which has no children
a Node with a value and two children called lefty and righty.

This is called an inductive type because later, we’ll be able to do mathematical induction on it.

Remember the Kotlin contains function:

fun Tree.contains(x: Int): Boolean=
  when (this) {
    Tree.Nil -> false
    is Tree.Node ->
      if (x          lefty.contains(x)
      } else if (value          righty.contains(x)
      } else {
         x==value
      }
  }

We can write the Kotlin contains function in Coq, too:

Fixpoint contains (x: nat) (t: tree): bool :=
    match t with
    | Nil=> false
    | Node lefty value righty=>
        if x         then contains x lefty
        else 
            if value             then contains x righty
            else x==y
    end.

A function is called a Fixpoint, if it contains recursion. The rest are syntactic differences between the two languages. For example, function application is done with a space instead of parentheses, which is common for the ML family of languages. Both functions do a pattern match on the tree, t. If the Tree is Nil, false is returned. Otherwise, it checks the value and continues the search on the appropriate branch.

Prove It Instead of Testing It

Instead of running a test, we can write a proof that executes at compile time.

Example example :=
  Node Nil 1 Nil.Theorem ExampleTreeContains1:
  contains 1 example=true.
Proof.
evaluate.

We can use the evaluate tool to evaluate the code, which results in the following goal:

- contains 1 example=true
+ true=true

This means we can use the same tool again to complete the proof:

Theorem ExampleTreeContains1:
  contains 1 example=true.
Proof.
evaluate.
same.
Qed.

Now our test is checked at compile time instead of at runtime. That was a pretty simple test. Let’s try something just slightly more complicated.

If our example tree is inside another tree, the tree should still contain 1.

Theorem NestedTreeContains1:
  forall
    (t: tree),
    t=Node example 2 (Node Nil 3 Nil)
  ->
    contains 1 t=true.

In this case, we can nail some hypotheses to the wall and get:

t: tree
H: t=Node example 2 (Node Nil 3 Nil)
----------------------------------------
contains 1 t=true

We need to break down the tree, let’s wreck t, which breaks t down into it’s two possible constructors: Nil and Node. Given we are exploring two possibilities, we also have to prove the goal for both possibilities. We use — to focus in on our first goal, where t is Nil.

H: Nil=Node example 2 (Node Nil 3 Nil)
----------------------------------------
- contains 1 t=true
+ contains 1 Nil=true

In this case, when we look at our hypothesis H, we have to say “wat!” I mean, this is impossible, right? Nil cannot be equal to a tree with some values. If we have one falsehood as a fact, then we can prove anything is true. Coq understands this, so we can just tell Coq wat, and it solves the subgoal for us.

Theorem NestedTreeContains1:
  forall (t: tree), 
    t=Node example 2 (Node Nil 3 Nil) 
  -> 
    contains 1 t=true.
Proof.
nail.
wreck t.
- wat.

This means we can focus on our second goal:

t1: tree
value: nat
t2: tree
H: Node t1 value t2=Node example 2 (Node Nil 3 Nil)
-----------------------------------------------------
- contains 1 t=true
+ contains 1 (Node t1 value t2)=true

We can now strip the constructor from both sides of H using wreck H into Ht1, Hv and Ht2, which gives us the following new hypotheses:

Ht2: t2=Node Nil 3 Nil
Hv: value=2
Ht1: t1=example

Now, we can do substitution using sub Hv, which changes our goal by replacing value with 2:

- contains 1 (Node t1 value t2)=true
+ contains 1 (Node t1 2 t2)=true

Coq can now partially evaluate this goal:

...
Ht1: t1=example
----------------------------------
- contains 1 (Node t1 2 t2)=true
+ contains 1 t1=true

Let’s substitute example into t1 using sub Ht1, to give us a familiar goal:

- contains 1 t1=true
+ contains 1 example=true

This is just the proof we had before ExampleTreeContains1 so we can complete our proof:

Theorem NestedTreeContains1:
  forall (t: tree),
    t=Node example 2 (Node Nil 3 Nil) 
  -> 
    contains 1 t=true.
Proof.
nail.
wreck t.
- wat.
- wreck H into Ht1, Hv and Ht2.
  sub Hv.
  evaluate.
  sub Ht1.
  just ExampleTreeContains1.
Qed.

These were very simple test cases that we have proven so far, but what about replacing a property-based test with a proof.

Proving a Property

Creating a proof for the property-based test we had before requires a Coq implementation of the insert function:

Fixpoint insert (value: nat) (t : tree) : tree :=
  match t with
  | Nil=> Node Nil value Nil
  | Node l tvalue r=>
    if value     then Node (insert value l) tvalue r
    else
      if tvalue       then Node l tvalue (insert tvalue r)
      else Node l value r
  end.

I purposefully made a mistake in this implementation that is hard to spot on first glance. Let’s see if our proof for our property-based test can catch the mistake:

Theorem contains_insert_prop: forall (t : tree) (value: nat),
  contains value (insert value t)=true.

We start by nailing some things to the wall:

t: tree
value: nat
----------------------------
contains value (insert value t)=true

Now, we have to do some math. Some of you might remember induction from mathematics. This is the tool we use for recursive structures. Using induction_on_tree t, we get two goals, one for each constructor of a tree: Nil and Node. The first case is our base case for induction:

value: nat
----------------------------
contains value (insert value Nil)=true

Coq can prove this using a combination of evaluate and same, so we can move on to our induction step case:

lefty: tree
tvalue: nat
righty: tree
value: nat
IHlefty: contains value (insert value lefty)=true
IHrighty: contains value (insert value righty)=true
-----------------------------------------------------
contains value (insert value (Node lefty tvalue righty))=true

Here, we have two induction hypotheses for each node in the tree, IHLefty and IHRighty. We have deconstructed our big goal tree, t, but also gained the knowledge that our property holds for the smaller left tree, lefty, and also holds for the smaller right tree, righty.

If we ask Coq to evaluate a bit of the goal, we can see it unfolds the contains function:

contains value
  (if value    then Node (insert value lefty) tvalue righty
   else
    if tvalue     then Node lefty tvalue (insert tvalue righty)
    else Node lefty value righty)=true

The code evaluation now depends on the comparison of value (the value being inserted) and tvalue (the value that is already in the tree). We can do a case comparison and look at all possibilities using compare value tvalue as C, which gives us three goals. Here’s the possibilities:

value=tvalue
value
tvalue

Focusing in on the first possibility, where value=tvalue, we find that Coq has already done the substitution for us as part of the compare, so our goal has also been updated with all the value being replaced by tvalue.

contains tvalue
  (if tvalue    then Node (insert tvalue lefty) tvalue righty
   else
    if tvalue     then Node lefty tvalue (insert tvalue righty)
    else Node lefty tvalue righty)=true

Coq can now evaluate the comparisons, like tvalue , which is false. This will result in the following:

contains tvalue (Node lefty tvalue righty)=true

Coq is smart enough to do more evaluation as part of evaluate and skip straight to:

true=true

We can finish this with the same tool and move on to the next goal, where value :

...
IHlefty: contains value (insert value lefty)=true
C: (value ------------------------------------------------
contains value
  (if value    then Node (insert value lefty) tvalue righty
   else
    if tvalue     then Node lefty tvalue (insert tvalue righty)
    else Node lefty value righty)=true

We can substitute comparison C into our goal using sub C, which allows Coq to evaluate the if statement; it will leave us with the following proof:

...
IHlefty: contains value (insert value lefty)=true
C: (value ----------------------------------------------------
contains value (Node (insert value lefty) tvalue righty)=true

We can now ask Coq to evaluate again using the contains function again:

...
IHlefty: contains value (insert value lefty)=true
C: (value ----------------------------------------------------
- contains value (Node (insert value lefty) tvalue righty)=true
+ (if value +   then contains value (insert value lefty)
+   else
+     if tvalue +     then contains value righty
+     else value==tvalue)=true

Now, we can do another substitution using sub C:

...
IHlefty: contains value (insert value lefty)=true
C: (value ----------------------------------------------------
contains value (insert value lefty)=true

We can now use our induction hypothesis since this is just IHLefty and we can move on to our final goal for the case, tvalue :

...
IHrighty: contains value (insert value righty)=true
C: (tvalue ----------------------------------------------------
contains value
  (if value    then Node (insert value lefty) tvalue righty
   else
    if tvalue     then Node lefty tvalue (insert tvalue righty)
    else Node lefty value righty)=true

We can start by substituting C and use our old theorem Lt_implies_not_Lt:

...
Lt_implies_not_Lt: forall {x: nat} {y: nat}, 
                     (x  y IHrighty: contains value (insert value righty)=true
C: (tvalue ---------------------------------------------------
contains value
  (if value    then Node (insert value lefty) tvalue righty
   else Node lefty tvalue (insert tvalue righty))=true

We can use Lt_implies_not_Lt to show that (value given C: (tvalue . We do this by calling Lt_implies_not_Lt as if it is a function, then passing C as a parameter and saving it in a new hypothesis C'. After that, we can see that tvalue and value are passed to it implicitly as x and y, respectively. Using call (Lt_implies_not_Lt C) as C’, we get the following:

...
IHrighty: contains value (insert value righty)=true
C: (tvalue + C': (value ---------------------------------------------------
contains value
  (if value    then Node (insert value lefty) tvalue righty
   else Node lefty tvalue (insert tvalue righty))=true

Now, we can substitute C' using sub C', and it will also evaluate the if expression, as shown below:

...
IHrighty: contains value (insert value righty)=true
C: (tvalue C': (value ---------------------------------------------------
contains value (Node lefty tvalue (insert tvalue righty))=true

We can now evaluate the goal further. Here’s what that looks like:

...
IHrighty: contains value (insert value righty)=true
C: (tvalue C': (value ---------------------------------------------------
(if value  then contains value lefty
 else
  if tvalue   then contains value (insert tvalue righty)
  else value==tvalue)=true

We can do some substitutions using sub C' and sub C. Here’s the code:

IHrighty: contains value (insert value righty)=true
---------------------------------------------------
contains value (insert tvalue righty)=true

At this point, I would expect to be able to use my induction hypothesis, but IHRighty is not the same as the goal. We will never be able to prove this goal because the code is incorrect.

RuPaul

It seems I made a Coq up!

If we look at our function again, we see that I copied tvalue instead of inserting value in certain cases.

Fixpoint insert (value: nat) (t : tree) : tree :=
  match t with
  | Nil=> Node Nil value Nil
  | Node l tvalue r=>
    if value     then Node (insert value l) tvalue r
    else
      if tvalue -       then Node l tvalue (insert tvalue r)
+       then Node l tvalue (insert value r)
      else Node l value r
  end.

If we fix the code and go back to our proof, we find that we can finish it using just IHRighty as expected:

Theorem contains_insert_prop : forall (t : tree) (value: nat),
  contains value (insert value t)=true.
Proof.
nail.
induction_on_tree t.
- evaluate.
  same.
- evaluate.
  compare value tvalue as C.
  + evaluate.
    same.
  + sub C.
    evaluate.
    sub C.
    just IHlefty.
  + sub C.
    call (Lt_implies_not_Lt C) as C'.
    sub C'.
    evaluate.
    sub C'.
    sub C.
    just IHRighty.
Qed.

Note: We focused on sub subgoals using a + operator. Coq allows us to use a combination of -, + and * characters to create a unique indentation string for each level.

It is pretty great that Coq found this bug, which might have been easily overlooked, but this was just a substitute for a property-based test. What if it was impossible to make this mistake in the first place because we began with the correct code?

Correct BST by Construction

One of the problems we had before was that the code allowed us to insert values into any tree, not just a Binary Search Tree (BST). We want functions that only take a BST as input and return a BST. Here’s an example:

Definition BSTinsert (ivalue : nat) (bst: BST): BST.

Note: We use Definition, which for the purposes of this article, is just another word for function or Fixpoint.

We want to create a BST type where the properties of a BST are always enforced. We want to trust that even the internal library code was correct without reading any of it. This means we want the BST type to also encode the properties of a BST.

We can describe a BST as a tree that satisfies the isBST property. We can do this using the curly braces that describe a subtype of tree, t.

Definition BST :={t | isBST t}.

In Coq, we can now describe the isBST inductive property:

Inductive isBST : tree -> Prop :=

All Nil trees are BSTs, so we can safely create a constructor for the Nil tree, as shown below:

| Nil_isBST :
    isBST Nil

We do need another constructor to safely build up BSTs. This is just the syntax, but we still need to fill in some properties to replace all the ...:

| Node_isBST :
    forall l x r,
      ...
      ...
      ...
      ...
    isBST (Node l x r).

The main property of a BST is that:

all the left children have to be less than their root
all the right children have to be greater than their root

Coq allows us to easily introduce new syntax, so we have created the and >> operators to express that all children are less than or greater than the root. This isn’t some magic. There are actually two functions that do some recursion to check that all values are less or more. How to add notation is out of the scope of this article.

| Node_isBST :
    forall l x r,
      l 
      r>> x ->
      ...
      ...
    isBST (Node l x r).

Finally, we also need to know that both the left and the right trees also satisfy the isBST property, so we can add that to get our full isBST property:

Inductive isBST : tree -> Prop :=
| Nil_isBST :
    isBST Nil
| Node_isBST :
    forall l x r,
      l 
      r>> x ->
      isBST l ->
      isBST r ->
    isBST (Node l x r).

It is impossible to construct a BST incorrectly. This BST is correct by construction, so we can focus on writing our type-safe insert function now.

Definition BSTinsert (ivalue : nat) (bst: BST): BST.

Here we define a function, but theorems are functions. This means that instead of coding a function, we can also use our tools to generate them. Our parameters become our hypotheses, and our return type is our goal.

ivalue: nat
bst: BST
-----------
BST

We can wreck bst into t and t_isBST to give us the tree and the isBST property separately.

ivalue: nat
t: tree
t_isBST: isBST t
-----------
BST

The tree we want to return is the tree where ivalue has been inserted. We can tell Coq this using the exists (insert ivalue t). Coq now knows the tree we want to return as part of our BST, but we still need to prove that the isBST property holds for that tree:

ivalue: nat
t: tree
t_isBST: isBST t
-----------
- BST
+ isBST (insert ivalue t)

The current hypothesis and goal look like a theorem we would like to prove separately, so let’s do that first. If we have a BST and we insert into it, we want to be guaranteed that the tree we get back is a BST.

Theorem isBSTinsert: forall (t : tree) (B: isBST t) (ivalue : nat),
  isBST (insert ivalue t).

We start by nailing some inputs to the wall using nail t B ivalue:

t: tree
B: isBST t
ivalue : nat
-------------------------------------------
isBST (insert ivalue t)

Next, we do induction_on_is_bst B to give us our two usual goals. The first one is our base case, which we can evaluate like this:

ivalue: nat
---------------------------
- isBST (insert ivalue Nil)
+ isBST (Node Nil ivalue Nil)

Now, we can wreck the isBST property into its four subproperties:

Nil
Nil>> ivalue
isBST Nil
isBST Nil

The first two is easy, so Coq will take care of it for us. The last two is just Nil_isBST, the constructor to show that a Nil tree is always a BST. This completes the proof for the base case. Now, we have to take on the induction step.

l: tree
bvalue: nat
r: tree
leftIsLess: l rightIsMore: r>> bvalue
isBSTl: isBST l
isBSTr: isBST r
ivalue: nat
IHlefty: isBST (insert ivalue l)
IHrighty: isBST (insert ivalue r)
------------------------------------------------------
isBST (insert ivalue (Node l bvalue r))

This induction created many induction hypotheses and other properties that we can use to construct the goal. We can evaluate the code to get the following:

...
leftIsLess: l rightIsMore: r>> bvalue
isBSTl: isBST l
isBSTr: isBST r
ivalue: nat
IHlefty: isBST (insert ivalue l)
IHrighty: isBST (insert ivalue r)
------------------------------------------------------
- isBST (insert ivalue (Node l bvalue r))
+ isBST
+ (if ivalue +  then Node (insert ivalue l) bvalue r
+  else
+   if bvalue +   then Node l bvalue (insert ivalue r)
+   else Node l ivalue r)

Now, we see a few comparisons, we can use compare ivalue bvalue as compare_ivalue_bvalue to break up our goal into three goals for the three comparison cases:

ivalue=bvalue
ivalue
bvalue

The first case where ivalue=bvalue Coq has already done some of the substitutions for us, so we can also evaluate a bit and get:

...
leftIsLess: l rightIsMore: r>> bvalue
isBSTl: isBST l
isBSTr: isBST r
IHlefty: isBST (insert ivalue l)
IHrighty: isBST (insert ivalue r)
+ compare_ivalue_bvalue: ivalue=bvalue
------------------------------------------
- ...
+ isBST (Node l bvalue r)

Now, we can wreck the isBST into its four subproperties to prove the following:

l , which is just leftIsLess
r>> bvalue, which is just rightIsMore
isBST l, which is just isBSTl
isBST r, which is just isBSTr

This means we have proven the case where ivalue=bvalue and we can move on to proving the case where (ivalue :

...
leftIsLess: l rightIsMore: r>> bvalue
isBSTl: isBST l
isBSTr: isBST r
IHlefty: isBST (insert ivalue l)
compare_ivalue_bvalue: (ivalue ------------------------------------------------------
isBST
  (if ivalue    then Node (insert ivalue l) bvalue r
   else
    if bvalue     then Node l bvalue (insert ivalue r)
    else Node l ivalue r)

We can sub compare_ivalue_bvalue, so that we get a much more simplified goal, as shown below:

...
leftIsLess: l rightIsMore: r>> bvalue
isBSTl: isBST l
isBSTr: isBST r
IHlefty: isBST (insert ivalue l)
compare_ivalue_bvalue: (ivalue ------------------------------------------------------
- ...
+ isBST (Node (insert ivalue l) bvalue r)

Now, we can again wreck the isBST property into its four subproperties to prove:

insert ivalue l bvalue
r>> bvalue, which is just rightIsMore
isBST (insert ivalue l), which is just IHLefty
isBST r, which is just isBSTr

We have one subproperty left to prove, and I created a helper theorem for us called all_less so we don’t have to do all the work. Here’s what that looks like:

...
all_less: forall {ivalue: nat} {t: tree} {bvalue: nat}
            (AL: t             (BIC: (ivalue           (insert ivalue t) leftIsLess: l compare_ivalue_bvalue: (ivalue ---------------------------------
insert ivalue l

When we apply all_less, we are asked to prove the parameters for the return value we want in the goal, so we get the following goals:

l , which is just leftIsLess
(ivalue , which is just compare_ivalue_bvalue

The other parameters in curly braces are all implicit and inferred for us. We have now proven the second comparison. The proof for the final comparison looks very similar, so we end up with the following:

Theorem isBSTinsert : forall (t : tree) (B: isBST t) (ivalue : nat),
  isBST (insert ivalue t).
Proof.
nail t B ivalue.
induction_on_is_bst B.
- nail.
  evaluate.
  wreck.
  + easy.
  + easy.
  + just Nil_isBST.
  + just Nil_isBST.
- evaluate.
  compare ivalue bvalue as compare_ivalue_bvalue.
  + evaluate.
    wreck.
    * just leftIsLess.
    * just rightIsMore.
    * just isBSTl.
    * just isBSTr.
  + sub compare_ivalue_bvalue.
    wreck.
    * apply all_less.
      --- just leftIsLess.
      --- just compare_ivalue_bvalue.
    * just rightIsMore.
    * just IHlefty.
    * just isBSTr.
  + sub compare_ivalue_bvalue.
    sub (Lt_implies_not_Lt compare_ivalue_bvalue).
    wreck.
    * just leftIsLess.
    * just (all_more rightIsMore compare_ivalue_bvalue).
    * just isBSTl.
    * just IHrighty.
Qed.

We can finish our BSTInsert function using our isBSTinsert theorem:

Definition BSTinsert
  (ivalue : nat) (bst: BST): BST.
nail.
wreck bst into t and t_isBST.
exists (insert ivalue t).
apply isBSTinsert.
just t_isBST.
Defined.

There we have it, a type-safe insert function that is correct by construction. The type checker won’t allow us to compile a function that doesn’t adhere to the BST’s properties.

Math Is a Tool for Programmers

Image Credit: Office Space (Movie)

While studying maths, I didn’t know the deep connection between maths and programming. I didn’t believe that proofs could have real-world industrial applications. How wrong I was! Maths is so useful in so many fields, so we’d be missing out if we didn’t take advantage of this.

Even more mind-blowing is that we saw that theorems and functions are interchangeable.

You can apply theorems like you apply functions
you can write proofs to implement functions instead of writing code
properties are just types that the type checker can check for us

If you want to learn more about this, you can search for Propositions as Types.

Getting Started

This was a teaser for what is possible with Coq using a very basic example. If you liked the taste of Coq, I recommend the following learning path.

The learning curve is steep, but I was lucky enough to find a study group to study this with me. We really liked the book the Little Typer, which taught us all about dependent types, which is the powerful type system that Coq is built upon. Then we found Coq in a Hurry, which was a great way to quickly start doing some Coq and get a feel for it. The CoqArt book was great for explaining the basics, and Certified Programming with Dependent Types was great for finishing up our introduction to Coq.

Alternatives

If you don’t like the taste of Coq, then there exist several alternative languages in which you can do proofs or use dependent types:

TLA+ is used by Amazon
Idris, Agda are very popular with Haskell programmers
Microsoft has Lean and F*
Isabelle was used to verify the web assembly spec

And there are many more.

Title of This Article

Coq is actually based on a branch of mathematics called constructive mathematics or, more specifically, the Calculus of Inductive Constructions, which is where we got the idea for the original title of the talk. This foundation is incredibly small, which means it is easy to trust that Coq itself is correct.

The “taste of Coq” is just something that almost slipped out during the talk. I noticed that the crowd was giggling whenever I said that this was just a taster. So I gave the crowd what they wanted and completed the obvious sentence.

Name

Why is it called Coq? It is funny but awkward. The rumour is that this is the French revenge. Coq was created in France, and for decades, they were stuck with the smallest computing unit, “bit,” which sounds like the equivalent of Coq in French. So it was about time for English speakers to also feel the awkwardness of saying inappropriate-sounding things while just trying to explain something about computing.

The far more likely story is that Thierry Coquand is the co-creator of Coq, and Coq is just the first part of his last name.

But why can’t both be true?

References

All the code is available on GitHub. We also created a construction toolbox to help with all the construction analogies. This means that the Coq we wrote looks slightly different than that found in the wild. The idea was that at this stage, it is more important to pique your interest in Coq than to teach you Coq since that would only be possible to do in a single article.

Thank you

Paul Cadman for creating this talk with me and organising the study group that made this all possible.
Cesar Tron-Lozai for pushing us to create this talk and attending our dry run.
London Type-Driven Development Study Group for taking this learning journey with us.

How to write correct code by construction using the Coq Proof Assistant