The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

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

Such is scheme is similar to the one generated in the case of mutual
inductive types.

While it is true that

  "induction t using foo_rect"

won't help a newcomer (or even more experienced Coq users ...)
because it won't be able to guess

          (Q := fun l => forall x, occ x l -> P x)
orelse    (Q := Forall_t P),

it would nonetheless be much better that the ones which are
actually generated by Coq now (which do not traverse the nesting).

Because that foo_rect you display here is powerful enough
to compute with the type of trees, in my opinion. Maybe with
the addition of a fixpoint equation in case you want to compute
with that principle.

DLW


-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQGcBAEBCAAGBQJX925NAAoJEF5s3tPiC7ucm3EMAJ28aJGkr75WdFbO+ivHv8r+
GniUcMDj43JbmYNS8x9O+1WeFPeCyTqbvPuVpgLqUcw1bP2yvfZf+wM3ufiLm16i
q1H51/7FaL7e2wTjxlq2ICiPqJWx9rq5dGVUog0pse8MKVak5HLlhhb9KN+p0XFd
MVtXvMCaM3f1SJK+FAIYsJ7q334jqPGHFwpX8XSYhCCWmJmUWLoaXsKvDnTJYsAm
tUFuw1sO2XmduqfTLeXtexmPjnyxgI+0WFPmTL0F8Qz3XywIfFc7DFFNnZlw8vTc
CPsRHgW8yAYFXcHqcCuePfR16U0bzwSKaEqIKK525Rij90NGO7ItKWGaeZZ9TGov
U5Wzbf1IH6IMVXJjCpGlk63a+0OtVfSsC90Ca0EvcqJyOfFXyWO75nFf1yFSQfsB
DE63awgq+0iOFQgSCdyRvREHDdSB98dYzECppnuW4eAvu/lTmKwqS2mm4ctiUW5r
qJ3w5gN01HqVOP43O2wcqkP9YMhhvATclckf5RIQQA==
=fZ/I
-----END PGP SIGNATURE-----