The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Vladimir Voevodsky wrote:
> It is arguable whether overusing induction and Prop is of any benefit for the 
> type-theoretic formalization of mathematics. In my experience one can 
> formalize everything with very few uses of [ Inductive ] and no use of Prop 
> at all.
>    

There are two questions here: inductive definitions vs. an impredicative 
universe.  I'm a believer in the usefulness of inductive definitions and 
increasingly a skeptic about the need for impredicativity.

> For example the use of inductive definition for "less or equal" on [ nat ] is 
> unnecessary. One can define boolean less or equal [ leb ] as a fix-point and then 
> define type-valued less or equal as [ Identity ( leb n m ) true ] . The proofs of all 
> the properties are rather straightforward.
>    

Your observation is similar to the one behind Ssreflect: many relations 
we care about are computable and can be formalized as computations.  
Many other relations that many of us work with regularly are not 
computable, such as almost anything dealing with execution of programs 
in Turing-complete languages.

It's probably possible to build a single parametrized inductive 
definition that can be instantiated to yield enough behavior for any 
interesting developments, but this also probably leads to a much less 
pleasant user experience.  I expect greater reliance on traditional 
first-order logic would have similar bad effects.  Inductive definitions 
just map well to the way that many of us think about math.