ListP t and ListI t are isomorphic: they have exactly the same constructors.
<prompt>Coq < 12 || 0 < </prompt>Check (NilP, NilI).
(NilP, NilI)
: (forall t : Type, ListP t) *
(forall t : Type, ListI t)
<prompt>Coq < 13 || 0 < </prompt>Check (ConsP, ConsI).
(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).
(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 t (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 ListP and ListI).
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 datatypesPolymorphism and Inductive datatypes for an example.
