The Coq mailing list

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

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.