The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 02 mai 2005, Roland Zumkeller wrote:

> I would be happy to see practical or philosophical arguments against 
> this approach:
> What is the advantage of defining "le" inductively?

I see these ones:

 -Induction. Induction/inversion principles built automatically from
inductive definitions are very useful. <ad> however you can now define
inductive principles from function definitions with Functional Scheme and
functional induction </ad>. 

 -Minimality. Your fixpoint definition contains a line with -> False,
because a function must be complete. You don't have this restriction when
you write an inductive definition, and thus an inductive definition (and
the induction associated principle) is more minimal.

 -Flexibility. Some properties can obviously not be defined by functions
because they are not decidable. Therefore people find more convenient to
define all their properties in the same style.

Pierre Courtieu