The Coq mailing list

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

Thanks!

---

From: "karsar" <karen.sarkisyan AT gmail.com>
To: "coq-club" <coq-club AT inria.fr>
Sent: Tuesday, 12 June, 2018 15:08:18
Subject: Re: [Coq-Club] Induction Principle

You may find useful information in http://adam.chlipala.net/cpdt/cpdt.pdf where author talks about induction principles

associated with the induction types, illustrates how to construct induction principle manually (you may get an understanding

what in essence automatic generation performs). He also brings an example where automatically generated induction

principle is not good enough and manually created one solves the task. And a plenty of other material.  

Best,

Karen

On Tue, Jun 12, 2018 at 8:52 PM Carmine Abate <carmine.abate AT inria.fr> wrote:

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.