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