The Coq mailing list

[Neil Ghani <Neil.Ghani AT cis.strath.ac.uk>]

Dear Coq Club

I have some questions about the treatment of induction in Coq.

1. I've been trying to write down an induction principle for the  
initial algebra of any functor, ie type operator with map operation.  
I know Coq generates induction principles for some functors and I  
wondered if it can generate an induction principle for any functor or  
if there are limitations on the class of functors for which induction  
principles can be generated.

2. What are the principles underlying the induction principles Coq  
generates? I believe they are added as axioms every time an  
inductive  data type is declared. Do they just look right or are they  
proven to be correct in a mathematical sense? If the later, could I  
get a response with a reference please?

All the best
Neil