The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 07/10/2016 01:44, Pierre Courtieu wrote:
> Can you give an example please? Is it really more complex that what
> mutual can give?

It depends. Mutual inductives need to have the same fixed parameters,
which is not the case for nested inductives. This requires a bit of
generalization over the context. Otherwise, this is straightforward, e.g.

Inductive foo := Foo : list foo -> foo.

should produce

Lemma foo_rect : forall (P : foo -> Type) (Q : list foo -> Type)
  (f : forall l, Q l -> (P (Foo l)))
  (f0 : Q nil)
  (f1 : forall x, P x -> forall l, Q l -> Q (cons x l)),
  forall x, P x.

If you want to do fancy stuff implying non-uniform parameters and
varying nested parameters, think for instance about the following
made-up inductive:

Inductive foo (A : Type) :=
| Foo : forall X, list (foo (A -> X)) -> foo A.

It should generate something of type:

Lemma foo_rect : forall
  (P : forall A, foo A -> Type)
  (Q : forall A X, list (foo (X -> A)) -> Type)
  (f : forall A X l, Q A X l -> P A (Foo A X l))
  (f0 : forall A X, Q A X nil)
  (f1 : forall A X x l, P (X -> A) x -> Q A X l -> Q A X (cons x l)),
  forall A (x : foo A), P A x.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature