In this new series of blog posts, we will be introducing Coq and Mi-Cho-Coq for proving Tezos smart contracts written in or compiled to Michelson. This series is structured as follows:
The context of this series on proving formally Michelson smart contracts having now been introduced, we can get started using Coq. We’ll first setup a working environment before introducing some of Coq’s core concepts. Please note that this chapter is heavily inspired by the Software Foundations’ first chapter on functional programming in Coq. It is much lighter, but provides many of the examples provided in Software Foundations as I found them very instructive. The explanations are ours however, as to provide a new insight, and we therefore strongly encourage our readers to go back to the Software Foundations’ first chapter after reading this article to get a deeper understanding of the concepts introduced here.
The simplest way to get started using Coq is through the CoqIDE, which we provide a Docker image for:
We can now hop into the container and launch the Coq IDE with some file:
In Coq, we define everything we’ll need to prove some proposition. Let’s define the boolean type, which take two values:
Easy! We can now define some functions operating on booleans. You’ll notice that Coq’s language is syntactically very similar to Ocaml’s, here’s how to implement a function negates its boolean input using pattern matching in Coq:
Similarly, we can define the and and or functions:
Which we can evaluate as follows:
Let’s now implement some tests for these functions:
Here, we’re proving test_orb1 as follows:
Of course, we don’t have to break lines between tactics:
Coq also lets us modify its reader to introduce useful new notations:
We can also define nested types, for example:
And functions operating on them:
Let’s now have some fun with natural numbers. We’ll define them in Coq as follows:
So a natural number is either O, representing 0, or the successor of any number n. This is an example of a recursive type. The number 0 is associated with O, 1 with S(O), 2 with S(S(O)), etc.
We can now easily define the predecessor function:
The predecessor of S(S(O)) is S(O), which is the successor of 0, which is obviously 1.
We can use recursive functions to define the plus and multiplication operations on natural numbers as follows:
Note that just as Ocaml required the keyword rec when defining a recursive function, Coq requires the Fixpoint one. Let’s prove that forall n in natural numbers, n + 0 = n:
Here things becomes interesting, we’ve used the keyword forall which allow us to prove our proposition of all the values of n allowed by its type. We use intros n to move n from the quantifier in the goal to the context of the current assumption. If you step through this code in the Coq IDE, you should see the following:
Let’s work through a more complex example. Here we want to prove that forall n, m in the natural numbers, the hypothesis n = m implies that n + n = m + m. We use the -> symbol between the hypothesis and its implication:
What we’ve done is introduced the hypothesis in the context of the current assumption and substituted it in the goal. Applying reflexivity then ends the proof.
Finally, it is now time to introduce case analysis. Say that we want to prove that forall b, c in booleans, b and c = c and b, we’ll need to essentially show that this holds for all four possible values of b and c. We can do this by using the destruct tactic. This tactic takes a variable that was introduced in the assumption context as argument, and, for a boolean, will create two subgoals: one where a = true, and one where a = false. Hence, by destructing both a and b and applying the reflexivity tactic, we can easily prove the following theorem:
This concludes our introduction to Coq. We have seen some of the most basic tactics, and will learn many more when we will encounter them while proving Michelson contracts. This chapter should have given you some rudimentary material to explore Coq in more detail by yourself by reading Software Foundations’ first chapter on functional programming in Coq, as well as further chapters from the same book.
In the next chapter, we will get started with Mi-Cho-Coq by proving the identity contract that stores outputs a new storage equal to its input.