An essential issue in the Vernacular is the ability to make inductive definitions. Inductive definitions are a very powerful feature of Coq, because they allow the user to define inductive data types even in a mutual way. For instance, in the slide we see the inductive definition of the set of natural numbers. This is the naive way to define a nat, and it works! We say that nat is a set that contains zero and that contains a successor function. Now inductive means that we are taking the least type satisfying those definitions. Well, better, it is the least set, the least type closed under the given operation. A very powerful thing about inductive definitions is that together with a definition Coq introduces automatically induction and recursion principles. This means that by just giving an inductive definition of a set, we get a principle of induction and a principle for recursive definitions. For instance, in this case, by just giving the inductive definition of nat, we get nat_ind - the induction principle over the natural numbers: For every property P, if it happens that P holds for 0, and from P holding on n we derive that P holds on the successor of n (S is the constructor used in the inductive definition), then the property P holds for every natural number. As we already mentioned before, not all inductive definitions are allowed, because we want to maintain strong normalisation. For instance, the inductive definition of this set D as (D ® false) ® D is not allowed, because D is not positive in this formula. By taking this definition we would break the strong normalisation property of Coq. Coq of course checks the constraint on this formula. It immediately discovered this formula was not of the required form and rejected the inductive definition.

---