Inductive types

Declaring inductive types

Inductive types can be defined using the Inductive keyword.

Below, we give the definition of natural numbers nat. They are literally the same as the ones from the standard library which we have been using until now.

The type nat is made of two constructors: O and S. We have O : nat and S n : nat if n : nat.

Rocq uses BNF (Backus-Naur-form) notation for inductive types:

Inductive nat : Type :=
| O : nat
| S : nat -> nat.

If you use Check (or hover the constants) you will see they have exactly the types we gave them in the description above: nat is a type (and thus of type Type), O is a nat, S has type nat -> nat, meaning it's a function taking a nat, say n, and returning another nat, called S n.

Check nat.
nat
     : Set
Check O.
O
     : nat
Check S.
S
     : nat -> nat

Elements of the type nat now consist exactly of O, S O, S (S O), and so on:

Check (S O).
S O
     : nat
Check (S (S O)).
S (S O)
     : nat

The Inductive command allows syntactic flexibility. We could also have written the following:

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

or without the first pipe (|) and the return type annotations:

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

In practice you get to pick the variant that suits you the most as they are anyway equivalent: they merely differ in how you write them, but produce the same definition.

You can actually check that they produce the same thing yourself by using the Print command on the inductive type nat:

Print nat.
Inductive nat : Set :=  O : nat | S : nat -> nat.

As the word inductive type hints, one can do proofs by induction about them. Mathematically, an inductive type is the smallest type closed under the type's constructors. You are already familiar with induction on natural numbers from the previous chapter. However, make sure that you are also familiar with the exact formulation of the induction principle:

Check nat_ind.
nat_ind
     : forall P : nat -> Prop,
       P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

As we have seen earlier, one can define recursive functions operating on inductive arguments with the Fixpoint keyword. We also already had a look at addition, but this time we'll look at its Rocq syntax. It operates by recursion on its first argument, n, looking at which constructor (O or S) is at its head. Operationally, it's looking at all the S on the left, and pushing them outside the addition, and once we reach O, the second argument m is returned.

Fixpoint add (n m : nat) {struct n} :=
  match n with
  | O => m
  | S n => S (add n m)
  end.

Rocq ensures that recursive functions are terminating, for reasons we will discuss later.

To ensure termination, recursion has to be performed on a structurally smaller argument. In the case of double from last week, there was only one argument so it was obvious which one had to decrease. This time, there is an ambiguity: it could be either n or m. The {struct n} annotation above tells Rocq that n is the one that is structurally decreasing.

Of course, it won't blindly trust us, there is a complex termination checker (sometimes called guard checker, and you will hear "guard condition" too) which will make sure this is indeed the case. For instance, if you were to suggest that m was structurally decreasing, Rocq would rightfully complain (which we indicate with the keyword Fail):

Fail Fixpoint add' (n m : nat) {struct m} :=
  match n with
  | O => m
  | S n => S (add' n m)
  end.
The command has indeed failed with message:
Recursive definition of add' is ill-formed.
In environment
add' : nat -> nat -> nat
n : nat
m : nat
n0 : nat
Recursive call to add' has principal argument equal to 
"m" instead of a subterm of "m".
Recursive definition is:
"fun n m : nat => match n with
                  | O => m
                  | S n0 => S (add' n0 m)
                  end".

The important bit of the error message is the one saying:

Recursive call to add' has principal argument equal to "m" instead of a subterm of "m".

In other words it's complaining about the recursive call being performed on m again.

Evaluating functions

It is possible to evaluate a function, such as the add function above by using the Eval command. Its first argument is an evaluation strategy (and we shall see more about that later), for now we use simpl, the very same we've been usinig inside proofs to simplify the goal. The term to evaluate is after the in:

Note how the following evaluates to fun m => m (the identity function):

Eval simpl in (fun m => add O m).
= fun m : nat => m
: nat -> nat

However, the following expression cannot be simplified using computation.

Eval simpl in (fun n => add n O).
= fun n : nat => add n O
: nat -> nat

The reason, is that computation really follows from the definition. We told Rocq that the main argument was the first (with {struct n}) and so it will not start computing until this one has a constructor in its head. A variable doesn't start with a constructor, so the expression is stuck.

This doesn't mean that add n O is different from O. There are indeed equal and we can prove it by induction, rather than by computation.

Lemma add_0 n :
  add n O = n.
n: nat
add n O = n
Proof.
n: nat
add n O = n
  induction n as [| n IHn].
add O O = O
n: nat
IHn: add n O = n
add (S n) O = S n
  -
add O O = O reflexivity.
  -
n: nat
IHn: add n O = n
add (S n) O = S n simpl.
n: nat
IHn: add n O = n
S (add n O) = S n rewrite IHn.
n: nat
IHn: add n O = n
S n = S n reflexivity.
Qed.

Let us now introduce an infix notations for add.

Infix "+" := add.

See how Rocq prints the lemma statement using + now!

Check add_0.
add_0
     : forall n : nat, n + O = n

Now, even if we still use add, Rocq will print the goal using +.

Lemma add_S n m :
  add n (S m) = S (add n m).
n, m: nat
n + S m = S (n + m)
Proof.
n, m: nat
n + S m = S (n + m)
  induction n as [| n IHn].
m: nat
O + S m = S (O + m)
n, m: nat
IHn: n + S m = S (n + m)
S n + S m = S (S n + m)
  -
m: nat
O + S m = S (O + m) reflexivity.
  -
n, m: nat
IHn: n + S m = S (n + m)
S n + S m = S (S n + m) simpl.
n, m: nat
IHn: n + S m = S (n + m)
S (n + S m) = S (S (n + m)) rewrite IHn.
n, m: nat
IHn: n + S m = S (n + m)
S (S (n + m)) = S (S (n + m)) reflexivity.
Qed.

We now define (truncating) subtraction on natural numbers. It is sometimes called monus.

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

Instead of using Infix to give a notation to sub we can also use the Notation command. It asks for more information and is sometimes tricky to use but it is very powerful. We will see more examples over the course of the lecture so don't worry too much about it.

Notation "n - m" := (sub n m).

An alternative to Eval simpl in e is Compute e. See what it does to the following two expressions.

Compute (S (S O) - S O). (* 2 - 1 = 1 *)
= S O
: nat
Compute (S O - S (S O)). (* 1 - 2 = 0 *)
= O
: nat

We can now prove a lemma involving addition and subtraction that we just defined.

Lemma add_sub n m :
  (n + m) - n = m.
n, m: nat
n + m - n = m
Proof.
n, m: nat
n + m - n = m
  induction n.
m: nat
O + m - O = m
n, m: nat
IHn: n + m - n = m
S n + m - S n = m
  -
m: nat
O + m - O = m simpl.
m: nat
m - O = m destruct m.
O - O = O
m: nat
S m - O = S m all: reflexivity.
  -
n, m: nat
IHn: n + m - n = m
S n + m - S n = m assumption.
Qed.

Above, we used a new construct all:, it tells Rocq to apply the tactic that follows (and only the one tactic) to all subgoals at this point. This is relative to the focused goals, so the successor case of the induction is not a target of reflexivity here. It will fail if the tactic fails in even just one of the goals.

Predicates, propositions and injectivity of constructors

In Rocq, everything is computational, including propositions.

We can define the following Boolean predicate testing whether a natural number is O or not.

Definition is_zerob (n : nat) : bool :=
  match n with
  | O => true
  | S n => false
  end.

But we can also produce directly a proposition asserting asserting whether the natural number is O or not. Pay attention to the use of Prop instead of bool and of capital True and False.

Definition is_zero (n : nat) : Prop :=
  match n with
  | O => True
  | S n => False
  end.

Prop is a bit like Type in that it classifies types, but there is a different intention behind Prop, its types are to be understood as propositions. Things like True, False and n = m are propositions, and we shall see more of them.

Of course, a proposition stating that n is O could equivalently be written as n = O as we have seen already. Similarly, we can express what it means to be different from O by writing n <> O, which is Rocq's way of writing n ≠ 0 (in fact, if you use Unicode with Rocq you can also write n ≠ 0 directly). This notation is nothing more than the negation of n = O, in other words it unfolds to (n = P) -> False.

We can use this to prove the fact that, in general, constructors are distinct. For nat this means that O and S n can always be distinguished.

Lemma S_O n :
  S n <> O.
n: nat
S n <> O
Proof.
n: nat
S n <> O

This can be proved manually

  intros E.
n: nat
E: S n = O
False

We use the change tactic to change the goal to something equivalent with respect to computation.

  change (is_zero (S n)).
n: nat
E: S n = O
is_zero (S n)

We can simplify again to get the old goal. This is in fact the reason why change succeeded in the first place.

  simpl.
n: nat
E: S n = O
False
  change (is_zero (S n)).
n: nat
E: S n = O
is_zero (S n)

Now that our goal is is_zero (S n) we want to use our hypothesis E : S n = O to get is_zero O instead. We can do this using the rewrite tactic which will replace occurrence of S n in the goal by the right-hand side of the equation, namely O.

  rewrite E.
n: nat
E: S n = O
is_zero O

Computation is now handy again, because is_zero O is much easier to prove than False. We simplify and then conclude.

  simpl.
n: nat
E: S n = O
True
  split.
Qed.

There is also a tactic to automatically discharge such goals: discriminate. Behind the scenes, it's essentially doing the above, by constructing a predicate that discriminates S n and O.

Lemma S_0' n :
  S n <> O.
n: nat
S n <> O
Proof.
n: nat
S n <> O
  discriminate.
Qed.

Say now we want to prove that S is injective. We can achieve this by using an auxiliary function pred such that pred (S n) = n (in other words, it is a left inverse to S). By congruence (f_equal) we can thus go from S n = S m to pred (S n) = pred (S m) which is then the same as n = m.

You can see here that it doesn't matter what value we choose for pred O. We're just going to pick O. In a sense it's only a partial predecessor.

Definition pred n :=
  match n with
  | O => O
  | S n => n
  end.

We can now prove that S is injective.

We will do it in several different ways to illustrate the possibilities. The first one uses change and is close in structure to the proof of the S_O lemma above.

Lemma S_inj n m :
  S n = S m -> n = m.
n, m: nat
S n = S m -> n = m
Proof.
n, m: nat
S n = S m -> n = m
  intros E.
n, m: nat
E: S n = S m
n = m
  change (pred (S n) = m).
n, m: nat
E: S n = S m
pred (S n) = m
  rewrite E.
n, m: nat
E: S n = S m
pred (S m) = m
  reflexivity.
Qed.

We could in fact do it without pred, in a way that's even closer to S_O.

Lemma S_inj_2 n m :
  S n = S m -> n = m.
n, m: nat
S n = S m -> n = m
Proof.
n, m: nat
S n = S m -> n = m
  intros E.
n, m: nat
E: S n = S m
n = m
  change (match S n with O => True | S k => k = m end).
n, m: nat
E: S n = S m
match S n with
| O => True
| S k => k = m
end
  rewrite E.
n, m: nat
E: S n = S m
m = m
  reflexivity.
Qed.

You may notice that after using rewrite, Rocq got rid of the pattern matching block (match) even we didn't ask it to do so with simpl. This will happen in some cases and we hope it's not too magical for your taste.

We can also use the f_equal lemma (not the tactic!).

Lemma S_inj_3 n m :
  S n = S m -> n = m.
n, m: nat
S n = S m -> n = m
Proof.
n, m: nat
S n = S m -> n = m
  Check f_equal.
f_equal
     : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y
n, m: nat
S n = S m -> n = m
  intros E.
n, m: nat
E: S n = S m
n = m
  apply (f_equal pred) in E.
n, m: nat
E: pred (S n) = pred (S m)
n = m
  assumption.
Qed.

Finally, we have tactics that do this automatically such as inversion.

Lemma S_inj_4 n m :
  S n = S m -> n = m.
n, m: nat
S n = S m -> n = m
Proof.
n, m: nat
S n = S m -> n = m
  intros E.
n, m: nat
E: S n = S m
n = m
  inversion E.
n, m: nat
E: S n = S m
H0: n = m
m = m
  reflexivity.
Qed.

Generalising induction hypotheses

Let us now try to prove things about functions operating on inductive types. We're going to start by defining a function for deciding equality between natural numbers.

Fixpoint eq_nat x y : bool :=
  match x, y with
  | O, O => true
  | O, S _ => false
  | S _, O => false
  | S x', S y' => eq_nat x' y'
  end.

We're going to prove that it indeed decides equality of natural numbers. Below, we again make use of the notation P <-> Q for logical equivalence. See above.

Lemma eq_nat_spec n m :
  eq_nat n m = true <-> n = m.
n, m: nat
eq_nat n m = true <-> n = m
Proof.
n, m: nat
eq_nat n m = true <-> n = m
  induction n as [ | n' IH].
m: nat
eq_nat O m = true <-> O = m
n', m: nat
IH: eq_nat n' m = true <-> n' = m
eq_nat (S n') m = true <-> S n' = m all: simpl.
m: nat
match m with
| O => true
| S _ => false
end = true <-> O = m
n', m: nat
IH: eq_nat n' m = true <-> n' = m
match m with
| O => false
| S y' => eq_nat n' y'
end = true <-> S n' = m

We made use of all: simpl. here to apply the simpl tactic to all subgoals, before even focusing them. all is called a goal selector by the way.

  -
m: nat
match m with
| O => true
| S _ => false
end = true <-> O = m destruct m.
true = true <-> O = O
m: nat
false = true <-> O = S m all: simpl.
true = true <-> O = O
m: nat
false = true <-> O = S m
    +
true = true <-> O = O split.
true = true -> O = O
O = O -> true = true all: reflexivity.

Notice reflexivity is able to conclude A -> 0 = 0 for any A.

    +
m: nat
false = true <-> O = S m split.
m: nat
false = true -> O = S m
m: nat
O = S m -> false = true all: intros E.
m: nat
E: false = true
O = S m
m: nat
E: O = S m
false = true all: discriminate E.

Here we provided E to discriminate to tell it which assumption was inconsistent (equating two distinct constructors).

  -
n', m: nat
IH: eq_nat n' m = true <-> n' = m
match m with
| O => false
| S y' => eq_nat n' y'
end = true <-> S n' = m destruct m.
n': nat
IH: eq_nat n' O = true <-> n' = O
false = true <-> S n' = O
n', m: nat
IH: eq_nat n' (S m) = true <-> n' = S m
eq_nat n' m = true <-> S n' = S m
    +
n': nat
IH: eq_nat n' O = true <-> n' = O
false = true <-> S n' = O split.
n': nat
IH: eq_nat n' O = true <-> n' = O
false = true -> S n' = O
n': nat
IH: eq_nat n' O = true <-> n' = O
S n' = O -> false = true all: discriminate.
    +
n', m: nat
IH: eq_nat n' (S m) = true <-> n' = S m
eq_nat n' m = true <-> S n' = S m

We are now stuck. The IH talks about S m, but we need it for m. Note that this always happens when a recursive function changes other arguments apart from its structural argument.

We give up for now:

Abort.

The proper way to deal with this is by generalising the induction hypothesis. We have to do this before we start perfoming induction. The reason we have to do this is because Rocq is trying to infer the property we prove by induction on its own: we only say we want to perform induction on n and it then tries to infer the property from the goal. Fortunately, the induction tactic also supports generalisation with the keyword in, as follows.

Lemma eq_nat_spec n m :
  eq_nat n m = true <-> n = m.
n, m: nat
eq_nat n m = true <-> n = m
Proof.
n, m: nat
eq_nat n m = true <-> n = m
  induction n as [ | n' IH] in m |- *.
m: nat
eq_nat O m = true <-> O = m
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
eq_nat (S n') m = true <-> S n' = m

The syntax is bit heavy: m |- * represents which information should Rocq take into account when generating the induction hypothesis. The turnstile |- is supposed to represent the whole proof goal, with the hypotheses on the left, and the proposition to prove on the right. We use * to indicate that we want to include the goal (which you always will want to do) and m on the left to indicate we generalise over it, and nothing else.

  -
m: nat
eq_nat O m = true <-> O = m destruct m.
eq_nat O O = true <-> O = O
m: nat
eq_nat O (S m) = true <-> O = S m all: simpl.
true = true <-> O = O
m: nat
false = true <-> O = S m
    +
true = true <-> O = O split.
true = true -> O = O
O = O -> true = true all: reflexivity.
    +
m: nat
false = true <-> O = S m split.
m: nat
false = true -> O = S m
m: nat
O = S m -> false = true all: discriminate.
  -
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
eq_nat (S n') m = true <-> S n' = m 

See how the IH is quantified for all m.

    destruct m.
n': nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
eq_nat (S n') O = true <-> S n' = O
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
eq_nat (S n') (S m) = true <-> S n' = S m all: simpl.
n': nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
false = true <-> S n' = O
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
eq_nat n' m = true <-> S n' = S m
    +
n': nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
false = true <-> S n' = O split.
n': nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
false = true -> S n' = O
n': nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
S n' = O -> false = true all: discriminate.
    +
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
eq_nat n' m = true <-> S n' = S m split.
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
eq_nat n' m = true -> S n' = S m
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
S n' = S m -> eq_nat n' m = true all: intros E.
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
E: eq_nat n' m = true
S n' = S m
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
E: S n' = S m
eq_nat n' m = true
      *
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
E: eq_nat n' m = true
S n' = S m apply IH in E.
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
E: n' = m
S n' = S m rewrite E.
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
E: n' = m
S m = S m reflexivity.
      *
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
E: S n' = S m
eq_nat n' m = true apply IH.
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
E: S n' = S m
n' = m inversion E.
n', m: nat
IH: forall m : nat, eq_nat n' m = true <-> n' = m
E: S n' = S m
H0: n' = m
m = m reflexivity.
Qed.

Booleans

We played with natural numbers quite a bit now. It's time to see other inductive types. We start with Booleans, which are even simpler.

Inductive bool := true | false.

Check true.
true
     : bool
Check bool.
bool
     : Set

Since bool is not recursive, the induction principle is a lot simpler. In this case, it makes sense to talk about case anlysis instead.

Check bool_ind.
bool_ind
     : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b

Again, since it's an inductive type, the constructors are disjoint.

Lemma true_false :
  true <> false.
true <> false
Proof.
true <> false
  discriminate.
Qed.

Cartesian product

We can define more types, such as the cartesian product.

We define product types inductively with one constructor taking two arguments.

Inductive prod X Y :=
| pair (x : X) (y : Y).

Note how the constructor pair takes 4 arguments:

Check pair.
pair
     : forall X Y : Type, X -> Y -> prod X Y

Namely types X and Y, and elements x : X and y : Y.

The first two arguments are real arguments that can be passed explicitly: types are first-class in Rocq.

Check pair nat.
pair nat
     : forall Y : Type, nat -> Y -> prod nat Y

Furthermore, types can appear at any position in arguments, unlike OCaml where the quantification is necessarily prenex.

Definition pair' X (x : X) Y (y : Y) :=
  pair X Y x y.

Check pair'.
pair'
     : forall X : Type, X -> forall Y : Type, Y -> prod X Y

Importantly, the type arguments have to be passed.

Fail Check pair' O O.
The command has indeed failed with message:
The term "O" has type "nat" while it is expected to have type "Type".

However, we can declare arguments as implicit using the Arguments command by marking implicit arguments with braces {} (sometimes called squigly brackets).

Arguments pair' {X} x {Y} y.

When an argument is implicit, Rocq tries to infer what it has to be, based on the other passed arguments. It involves a process called unification. If we build the pair (O,O) then both types have to be nat and Rocq is able to figure it out.

Check pair' O O.
pair' O O
     : prod nat nat

We can use the following command to force Rocq to print implicit arguments.

Set Printing Implicit.

There we can see the nat that have been inferred.

Check pair' O O.
@pair' nat O nat O
     : prod nat nat

We go back to not printing implicit arguments.

Unset Printing Implicit.

We can define the first projection by pattern matching. We mark arguments as implicit directly, but we could have used Arguments later instead.

Definition fst {X Y} (p : prod X Y) : X :=
  match p with
  | pair _ _ x y => x
  end.

This is just the tip of the iceberg and we shall see more interesting and complicated example of inductive types soon.

For now, let us focus on exercises. 😉