Mi-cho-coq tutorial • A quick introduction to Coq

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:

 
• 01. Formal proving: What is it about, what are Coq and Mi-Cho-Coq, and why will we need them.
 
• 02. A quick introduction to Coq
 
• 03. A quick introduction to Mi-Cho-Coq: proving our first Michelson smart contract.
 
• 04. Proving the increment contract
 
• 05. Proving if conditions.
 
• 06. Proving a token minting entrypoint

Chapter II

Introduction

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.

Getting started: launching the Coq IDE

The simplest way to get started using Coq is through the CoqIDE, which we provide a Docker image for:

host $ git clone git@gitlab.com:equisafe/nyx.git
host $ cd nyx/mi-cho-coq/
host $ docker-compose up -d
host $ docker ps
CONTAINER ID        IMAGE
dbafd3fc597d        thomasbinetruy/eqs-nyx:michocoq

We can now hop into the container and launch the Coq IDE with some file:

host $ docker exec -it dbafd3fc597d /bin/bash
container $ eval $(opam env)
container $ ls
deposit.v simple.v
container $ coqide simple.v

The Coq language

In Coq, we define everything we’ll need to prove some proposition. Let’s define the boolean type, which take two values:

Inductive bool : Type :=
  | true
  | false.

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:

Definition negb (b:bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

Similarly, we can define the and and or functions:

Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.
Definition orb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

Which we can evaluate as follows:

Compute andb true false.
(* ==> false: bool *)

Let’s now implement some tests for these functions:

Example test_orb1: (orb true false) = true.
Proof. 
  simpl.          (* ===> true = true *)
  reflexivity.    (* ===> no more subgoals *)
Qed.

Here, we’re proving test_orb1 as follows:

 
1. We simplify both side using the simpl tactic, which results in true = true
 
2. We then end the proof by asserting that both sides are equal using the reflexivity tactic.

Of course, we don’t have to break lines between tactics:

Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.

Coq also lets us modify its reader to introduce useful new notations:

Notation "x & y" := (andb x y).
Notation "x || y" := (orb x y).
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

We can also define nested types, for example:

Inductive rgb : Type :=
  | red
  | green
  | blue.
Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

And functions operating on them:

Definition monochrome (c : color) : bool :=
  match c with
  | black => true
  | white => true
  | primary p => false
  end.

Natural numbers

Let’s now have some fun with natural numbers. We’ll define them in Coq as follows:

Inductive nat : Type :=
  | O
  | S (n : nat).

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:

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

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:

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O => m
    | S n' => S (plus n' m)
  end.

Fixpoint mult (n m : nat) : nat :=
  match n with
    | O => O
    | S n' => plus m (mult n' m)
  end.

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:

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

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:

1 subgoal
______________________________________(1/1)
forall n : nat, 0 + n = n

(* intros n *)

1 subgoal
n : nat
______________________________________(1/1)
0 + n = n

(* simpl *)

1 subgoal
n : nat
______________________________________(1/1)
n = n

(* reflexivity *)

No more subgoals.

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:

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.
Proof.
  (* 
    1 subgoal
    ______________________________________(1/1)
    forall n m : nat, n = m -> n + n = m + m
  *)

  (* move both quantifiers into the context: *)
  intros n m.

  (* 
    1 subgoal
    n, m : nat
    ______________________________________(1/1)
    n + n = m + m
  *)

  (* move the hypothesis into the context: *)
  intros H.

  (*
    1 subgoal
    n, m : nat
    H : n = m
    ______________________________________(1/1)
    n + n = m + m
  *)

  (* rewrite the goal using the hypothesis: *)
  rewrite -> H.

  (*
    1 subgoal
    n, m : nat
    H : n = m
    ______________________________________(1/1)
    m + m = m + m
  *)
  reflexivity. 

  (*
    No more subgoals.
  *)
Qed.

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:

Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.

Conclusion

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.

Go to the next part :

• Mi-cho-coq tutorial • Proving our first Michelson smart contract