2.1  Data Types as Inductively Defined Mathematical Collections

All the notions which were studied until now pertain to traditional mathematical logic. Specifications of objects were abstract properties used in reasoning more or less constructively; we are now entering the realm of inductive types, which specify the existence of concrete mathematical constructions.

2.1.1  Booleans

Let us start with the collection of booleans, as they are specified in the Coq's Prelude module:

Such a declaration defines several objects at once. First, a new Set is declared, with name bool. Then the constructors of this Set are declared, called true and false. Those are analogous to introduction rules of the new Set bool. Finally, a specific elimination rule for bool is now available, which permits to reason by cases on bool values. Three instances are indeed defined as new combinators in the global context: bool_ind, a proof combinator corresponding to reasoning by cases, bool_rec, an if-then-else programming construct, and bool_rect, a similar combinator at the level of types. Indeed:

Let us for instance prove that every Boolean is true or false.

We use the knowledge that b is a bool by calling tactic elim, which is this case will appeal to combinator bool_ind in order to split the proof according to the two cases:

It is easy to conclude in each case:

Indeed, the whole proof can be done with the combination of the simple induction tactic, which combines intro and elim, with good old auto:

2.1.2  Natural numbers

Similarly to Booleans, natural numbers are defined in the Prelude module with constructors S and O:

The elimination principles which are automatically generated are Peano's induction principle, and a recursion operator:

Let us start by showing how to program the standard primitive recursion operator prim_rec from the more general nat_rec:

That is, instead of computing for natural i an element of the indexed Set (P i), prim_rec computes uniformly an element of nat. Let us check the type of prim_rec:

Oops! Instead of the expected type nat->(nat->nat->nat)->nat->nat we get an apparently more complicated expression. Indeed the type of prim_rec is equivalent by rule β to its expected type; this may be checked in Coq  by command Eval Cbv Beta, which β-reduces an expression to its normal form:

Let us now show how to program addition with primitive recursion:

That is, we specify that (addition n m) computes by cases on n according to its main constructor; when n = O, we get m; when n = S p, we get (S rec), where rec is the result of the recursive computation (addition p m). Let us verify it by asking Coq to compute for us say 2+3:

Actually, we do not have to do all explicitly. Coq provides a special syntax Fixpoint/match for generic primitive recursion, and we could thus have defined directly addition as:



For the rest of the session, we shall clean up what we did so far with types bool and nat, in order to use the initial definitions given in Coq's Prelude module, and not to get confusing error messages due to our redefinitions. We thus revert to the state before our definition of bool with the Reset command:

2.1.3  Simple proofs by induction

Let us now show how to do proofs by structural induction. We start with easy properties of the plus function we just defined. Let us first show that n=n+0.

What happened was that elim n, in order to construct a Prop (the initial goal) from a nat (i.e. n), appealed to the corresponding induction principle nat_ind which we saw was indeed exactly Peano's induction scheme. Pattern-matching instantiated the corresponding predicate P to fun n:nat => n = n 0+, and we get as subgoals the corresponding instantiations of the base case (P O) , and of the inductive step forall y:nat, P y -> P (S y). In each case we get an instance of function plus in which its second argument starts with a constructor, and is thus amenable to simplification by primitive recursion. The Coq tactic simpl can be used for this purpose:

We proceed in the same way for the base step:

Here auto succeeded, because it used as a hint lemma eq_S, which say that successor preserves equality:

Actually, let us see how to declare our lemma plus_n_O as a hint to be used by auto:

We now proceed to the similar property concerning the other constructor S:

We now go faster, remembering that tactic simple induction does the necessary intros before applying elim. Factoring simplification and automation in both cases thanks to tactic composition, we prove this lemma in one line:

Let us end this exercise with the commutativity of plus:



Here we have a choice on doing an induction on n or on m, the situation being symmetric. For instance:

Here auto succeeded on the base case, thanks to our hint plus_n_O, but the induction step requires rewriting, which auto does not handle:

2.1.4  Discriminate

It is also possible to define new propositions by primitive recursion. Let us for instance define the predicate which discriminates between the constructors O and S: it computes to False when its argument is O, and to True when its argument is of the form (S n):

Now we may use the computational power of Is_S in order to prove trivially that (Is_S (S n)):

But we may also use it to transform a False goal into (Is_S O). Let us show a particularly important use of this feature; we want to prove that O and S construct different values, one of Peano's axioms:

First of all, we replace negation by its definition, by reducing the goal with tactic red; then we get contradiction by successive intros:

Now we use our trick:

Now we use equality in order to get a subgoal which computes out to True, which finishes the proof:

Actually, a specific tactic discriminate is provided to produce mechanically such proofs, without the need for the user to define explicitly the relevant discrimination predicates:

2.2  Logic programming

In the same way as we defined standard data-types above, we may define inductive families, and for instance inductive predicates. Here is the definition of predicate ≤ over type nat, as given in Coq's Prelude module:

This definition introduces a new predicate le:nat->nat->Prop, and the two constructors le_n and le_S, which are the defining clauses of le. That is, we get not only the “axioms” le_n and le_S, but also the converse property, that (le n m) if and only if this statement can be obtained as a consequence of these defining clauses; that is, le is the minimal predicate verifying clauses le_n and le_S. This is insured, as in the case of inductive data types, by an elimination principle, which here amounts to an induction principle le_ind, stating this minimality property:

Let us show how proofs may be conducted with this principle. First we show that n≤ m ⇒ n+1≤ m+1:

What happens here is similar to the behaviour of elim on natural numbers: it appeals to the relevant induction principle, here le_ind, which generates the two subgoals, which may then be solved easily with the help of the defining clauses of le.

Now we know that it is a good idea to give the defining clauses as hints, so that the proof may proceed with a simple combination of induction and auto.

We have a slight problem however. We want to say “Do an induction on hypothesis (le n m)”, but we have no explicit name for it. What we do in this case is to say “Do an induction on the first unnamed hypothesis”, as follows.

Here is a more tricky problem. Assume we want to show that n≤ 0 ⇒ n=0. This reasoning ought to follow simply from the fact that only the first defining clause of le applies.

However, here trying something like induction 1 would lead nowhere (try it and see what happens). An induction on n would not be convenient either. What we must do here is analyse the definition of le in order to match hypothesis (le n O) with the defining clauses, to find that only le_n applies, whence the result. This analysis may be performed by the “inversion” tactic inversion_clear as follows: