The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Adam, Jason,

i had a bad gut feeling about such a mechanism, since it would be a partial
relation rather than a total function. Thanks for providing the background
info and a name for this kind of bad gut feeling ;-) Currently I use a type
class to pair an inductive with its induction principle. This works fine, but
I have another problem with this. I am experimenting with inductive
structures, which allow the embedding of custom record types. I first tried to
embed type and value descriptions of the record type in the inductive
structure. This works, but leads to rather lengthy proof goals which make it
difficult to debug proofs. So I started to experiment with embedding user
supplied native Coq record types. For this I need the induction principle of
the user supplied record type to define the semantic relation of the whole
structure. The problem now is that the sematics depends on the supplied
induction principle. The automatically generated induction principle of simple
record types leads to the kind of sematics I want, so I thought about ways to
connect a type to its "default" induction principle.

I think the method Jason suggested, to construct the induction principle from
the type, might be the best solution for my problem. It might not only
restrict the induction principles to the kind of induction principles I want,
but also the types to those types for which such an induction principle works.
In the end I want to restrict parametricity to restrict the semantics of the
whole structure to something I can foresee. What I don't understand as yet is
what happens if I supply a type to Jason's function for which the induction
principle doesn't work. I will experiment with Jason's suggestion and see if
it helps me to come to a deeper understanding of this.

Thanks for your help & best regards,

Michael