ListP t and
ListI t are isomorphic: they have exactly the same constructors.
<prompt>Coq < 12 || 0 < </prompt>Check (NilP, NilI).
: (forall t : Type, ListP t) *
(forall t : Type, ListI t)
<prompt>Coq < 13 || 0 < </prompt>Check (ConsP, ConsI).
: (forall t : Type, t -> ListP t -> ListP t) *
(forall t : Type, t -> ListI t -> ListI t)
However Coq generates different induction principles.
<prompt>Coq < 14 || 0 < </prompt>Check (ListP_ind, ListI_ind).
: (forall (t : Type) (P : ListP t -> Prop),
P (NilP t) ->
(forall (t0 : t) (l : ListP t), P l -> P (ConsP t t0 l)) ->
forall l : ListP t, P l) *
(forall P : forall T : Type, ListI T -> Prop,
(forall t : Type, P t (NilI t)) ->
(forall (t : Type) (t0 : t) (l : ListI t),
P t l -> P t (ConsI t t0 l)) ->
forall (T : Type) (l : ListI T), P T l)
The induction principle of
ListI requires the property to be parameteric in the element type (
P : forall T, ListI T -> Prop) whereas the induction principle of
ListP can be instantiated at any type
P : ListP t -> Prop). This is a weakness of Coq's front-end, in that it is not smart about non-uniform recursive types; you can manually define the same induction principle (the typechecker accepts it, which is unsurprising given that it is
ListP_ind transformed by the obvious isomorphism between
The parametric form
ListP is simpler and easier to use out of the box. The
ListI form can generalize to non-uniform recursion, where the parameters in the recursive calls are not the original. See Polymorphism and Inductive datatypes for an example.