Different induction principles for Prop and Type

Link:

https://stackoverflow.com/q/39683390

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

Arguments eq {A}%type_scope _ _
Arguments eq_refl {A}%type_scope {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

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

Arguments S _%nat_scope

    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

Arguments list _%type_scope
Arguments nil {A}%type_scope
Arguments cons {A}%type_scope a l%list_scope
  (where some original arguments have been renamed)

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

  • Vectors are a different:

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

Arguments VectorDef.t _%type_scope _%nat_scope
Arguments VectorDef.nil _%type_scope
Arguments VectorDef.cons _%type_scope _ _%nat_scope _

    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).

A: Updated link: https://coq.inria.fr/refman/user-extensions/proof-schemes.html#generation-of-induction-principles-with-scheme