How to think of inductive types?

Using Rocq
1

Let’s consider this definition for a type for natural numbers:

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

I used to read this definition as

t is an inductive type with two constructors - O and S, the latter taking a term of type t as a parameter.

and from that, I used to conclude something like

All the terms of type t are of the form S (S ... (S O) ... ), namely a bunch of (optional) S’s, followed by a terminating O.

In fact, I based my intuition for induction on the statement above, but the statement is clearly incorrect, cus other terms can also have the type t, for example (fun x : t => x) O. But nonetheless, the “base” terms of t, those on which no more reductions can be performed, are indeed a bunch of optional S’s, terminated by an O, right?

So, is there a notion of “values” of a type in Rocq? Maybe something like a term that isn’t reducible any further? I’ve seen the term inhabitant used at some places in the reference manual but I’m not sure what that means.

And, when you guys read a statement of the form forall n : t, n = n, do you think of these n’s as only the sequence of S’s followed by an O, or do you also think about terms like function applications, let-in expressions, etc? I suppose it doesn’t make much of a difference, though, because all of those terms are reducible to these “base” terms, so proving a proposition for the base terms is “enough” - but I still want to know how you guys “read” these inductive definitions and these propositions involving the universal quantifier.

Thanks a lot.

2

The answer will be kind of similar to the one in the other post: In the empty context and modulo convertibility, every term of type t is of the form S ... S O. So, this is the case for (fun x => x) O, which is just O modulo convertibility. And this is not the case for n in forall n, n = n since the context is not empty (it contains n). That said, n is provably indistinguishable from a term of the form S ... S O (which is what it means to reason by induction onn).

1 Like
3

I don’t know much about the internal logic of the Rocq-Prover or type theory in general, so this answer might be flawed. With that said, I hope to discuss some related ideas and help you find relevant materials to read.

For the first part, I think what you are looking for is normal forms and/or canonical forms of inductive data types. CIC, the internal type theory, was proven to be strong normalizing. Therefore closed (with no free variable) expressions of any inductive data type can be normalized (with finitely many reductions) into finite sequences (or finite trees).

As for the second part, you can check the type of the automatically generated recursion eliminator and induction principle.

If you are using CoqIDE, after sending a inductive data type definition, you will get some feedback like:

Nat.rect is defined
Nat_ind is defined
Nat_rec is defined
Nat_sind is defined

For example, Check nat_ind and Check nat_rect will give

nat_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, P n

nat_rect
     : forall P : nat -> Type,
       P 0 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, P n

The mathematical induction and the recursion principle.

Of course, this only concerns the “type” being correct.
The property that “the computation defined by these inductions are terminating”, I believe, is guaranteed by the normalization property.

1 Like
4

That is true, but kind of trivially. Termination and normalization are so intricately related in Rocq (and elsewhere in type theory) that they are fundamentally the same thing, so people will interchangeably use one word for the other. (Thus, “termination is guaranteed by the termination property”.)

So, it might be more accurate and useful to tell that the termination of recursive definitions in Rocq comes from the decrease of the recursive argument according to a well-founded order derived from the positivity constraint on the inductive types, combined with a syntactic check on the form of the recursive definition.

As for why termination matters, even before talking about normalization, it is because there would be trivial proofs of False otherwise. An example is ((fix loop (x:unit): False := loop x) tt), which fails the syntactic check mentioned above.

2 Likes
5

Thanks for the comment. Now I can see thatt my response is somewhat misleading.

What I am trying to suggest here is that by appealing to induction principles of inductive data types one can inhabit an universally quantified type.
For example, given H_base : P 0 and H_step : forall n, P n -> P (S n) one can form a term nat_ind H_base H_step : forall n, P n, according to the typing rule.

However, this only covers the type level or the syntax. The semantics is left unexamined. To establish the correctness of the inductive principle itself, one have to show some termination property.

And the reason for mention normalization property again is because well-foundedness of nat_ind is not enough. We need to show expression of natural number type is normalising. Otherwise, running prove_forall_n_Pn diverge where diverge : nat but is non-terminating will not give a value of P diverge type. Luckily, we cannot define a diverging term in Rocq.