The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, September 24, 2011 01:32:34 AM you wrote:
> Hi
> 
> I read what you wrote below and was interested in what you were writing
> about induction over inductively defined subsets. Can you say a little
> more about what you see the problems are?

It's just that "induction on a proposition" isn't really part of the standard 
mathematical language.

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".  At least until 
they get to the point where they're more comfortable with Curry-Howard.
-- 
Daniel