The Coq mailing list

[Carmine Abate <carmine.abate AT inria.fr>]

Formally my question can be formulated as 

" given an inductive type \alpha, (like the one I wrote previously) 
  what is its induction principle \alpha_ind? 
  and what is a term with type \alpha_ind? " 

Coq Art is useful as it shows many examples 
(and maybe I can try to write the rule by myself),
but is there some reference showing a general rule?

Thanks, 

Carmine


----- Original Message -----
> From: "Pierre Courtieu" 
> <pierre.courtieu AT gmail.com>
> To: "coq-club" 
> <coq-club AT inria.fr>
> Sent: Tuesday, 12 June, 2018 14:19:42
> Subject: Re: [Coq-Club] Induction Principle

> Hi,
> I don't know what you mean by "write the term". Do you mean "prove"?
> If yes then you can look at the definition of, say, nat_ind by doing:
> "Print nat_ind."
> You get something like this.
> 
> fix F (n : nat) : P n :=
>  match n as n0 return (P n0) with
>  | 0 => f
>  | S n0 => f0 n0 (F n0)
>  end.
> 
> Notice the form "fix F n .. := match n with ....end"
> This Fix + match is the core structure of the proofs of induction
> principles: it is the nominal application of the elimination mechanism
> at the heart of CIC.
> 
> Hope this helps.
> P.