Different induction principles for Prop and Type

Question

I noticed that Coq synthesizes different induction principles on equality for Prop and Type. Does anybody have an explanation for that?

Equality is defined as

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

And the associated induction principle has the following type:

eq_ind
 : forall (A : Type) (x : A) (P : A -> Prop),
   P x -> forall y : A, x = y -> P y

Now let's define a Type pendant of eq:

Inductive eqT {A:Type}(x:A):A->Type:= eqT_refl: eqT x x.

The automatically generated induction principle is

eqT_ind
 : forall (A : Type) (x : A) (P : forall a : A, eqT x a -> Prop),
   P x (eqT_refl x) -> forall (y : A) (e : eqT x y), P y e

Answer 1

Note: I'm going to use _rect principles everywhere instead of _ind, since _ind principles are usually implemented via the _rect ones.

Type of eqT_rect

Let's take a look at the predicate P. When dealing with inductive families, the number of arguments of P is equal to the number of non-parametric arguments (indices) + 1.

Let me give some examples (they can be easily skipped).

• Natural numbers don't have parameters at all:

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

  So, the predicate P will be of type nat -> Type.

• Lists have one parametric argument (A):

  Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A.
  

  Again, P has only one argument: P : list A -> Type.

• Vectors are a different:

  Inductive vec (A : Type) : nat -> Type :=
    nil : vec A 0
  | cons : A -> forall n : nat, vec A n -> vec A (S n).
  

  P has 2 arguments, because n in vec A n is a non-parameteric argument:

  P : forall n : nat, vec A n -> Type
  

The above explains eqT_rect (and, of course, eqT_ind as a consequence), since the argument after (x : A) is non-parametric, P has 2 arguments:

P : forall a : A, eqT x a -> Type

which justifies the overall type for eqT_rect:

eqT_rect
     : forall (A : Type) (x : A) (P : forall a : A, eqT x a -> Type),
       P x (eqT_refl x) -> forall (y : A) (e : eqT x y), P y e

The induction principle obtained in this way is called a maximal induction principle.

Type of eq_rect

The generated induction principles for inductive predicates (such as eq) are simplified to express proof irrelevance (the term for this is simplified induction principle).

When defining a predicate P, Coq simply drops the last argument of the predicate (which is the type being defined, and it lives in Prop). That's why the predicate used in eq_rect is unary. This fact shapes the type of eq_rect:

eq_rect : 
  forall (A : Type) (x : A) (P : A -> Type),
         P x -> forall y : A, x = y -> P y

How to generate maximal induction principle

We can also make Coq generate non-simplified induction principle for eq:

Scheme eq_rect_max := Induction for eq Sort Type.

The resulting type is

eq_rect_max :
  forall (A : Type) (x : A) (P : forall a : A, x = a -> Type),
         P x eq_refl -> forall (y : A) (e : x = y), P y e

and it has the same structure as eqT_rect.

References

For more detailed explanation see sect. 14.1.3 ... 14.1.6 of the book "Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions)" by Bertot and Castéran (2004).