Ind-s and Rec-s of types

When we define an inductive type in Coq, a few things other than the type and its constructors get defined.

Inductive type := Ttype.

(* type is defined *)
(* type_rect is defined *)
(* type_ind is defined *)
(* type_rec is defined *)
(* type_sind is defined *)

These are the induction principle of the type tailored to Prop, Set, Type and SProp.

For example, in the case of nat:

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

Check nat_rec.
(*
nat_rec
     : forall P : nat -> Set,
       P 0 ->
       (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
*)

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

Check nat_sind.
(*
nat_sind
     : forall P : nat -> SProp,
       P 0 ->
       (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
*)

I wonder why they needed separate lemmas for Set and Type..

Name Type used
ind Prop
rect Type
rec Set
sind SProp

For example, what nat_ind says is this:

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

If a proposition P holds over 0 (which is the base case for nat), and if know that P holds for n+1 if it holds for any n, then P is true for all nat.

And in the case of list:

list_ind
     : forall (A : Type) (P : list A -> Prop),
       P nil ->
       (forall (a : A) (l : list A), P l -> P (a :: l)%list) ->
       forall l : list A, P l

list_ind is indicative of the fact that

If:

then:

By the way, the ind-s and rec-s won't get defined when we make a coinductive type. Because they are potentially infinite.

CoInductive t A :=
| CNil: t A
| CCons: A -> t A -> t A.

(* t is defined *)

References