The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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.

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.

Vladimir.







On Sep 24, 2011, at 1:09 PM, Adam Chlipala wrote:

> Daniel Schepler wrote:
>> It's just that "induction on a proposition" isn't really part of the 
>> standard
>> mathematical language.
>>   
> 
> Perhaps you can view it as a public service task to help change that 
> deficiency? ;)
> 
>> As an example, take "<=" on the natural numbers.  In Coq,<= is defined so 
>> that
>> for fixed a, { b:nat | a<= b } is the smallest subset of nat which 
>> contains a,
>> and such that whenever b is in the set, succ(b) is also.
>> 
>> Now consider the problem of proving that<= is transitive, i.e. if a<= b and
>> b<= c then a<= c.  In Coq, the usual way to prove this would be "by
>> induction on b<= c".  In standard mathematical language, this proof would 
>> be
>> translated as: suppose a<= b.  Then { c:nat | a<= c } contains b; and by
>> definition, whenever c is in that set, succ(c) is also.  Since { c:nat | 
>> b<= c
>> } is the smallest such set, it follows that { c:nat | b<= c } is a subset 
>> of
>> { c:nat | a<= c }.  We have now proved that a<= b ->  ({ c:nat | b<= c } is
>> a subset of { c:nat | a<= c }), and if we unfold the definition of subset, 
>> we
>> get exactly the desired transitivity property.
>> 
>> So for mathematicians, it's probably easiest to think of "induction on a 
>> Prop"
>> as shorthand for this style of argument, "the set of values satisfying my
>> desired conclusion contains the generators and satisfies the closure 
>> relations
>> defining the set of values corresponding to some hypothesis".
>>   
> 
> Does any significant fraction of working mathematicians get into this level 
> of detail about "<="?  I would expect that instead they use perhaps normal 
> mathematical induction on "a" and don't sweat the details.