Explanation
This is the most typical kind of induction. The main point worth remarking
upon is that this proof needs several lemmas about the natural numbers. Two
of these are the associative and commutative laws for addition, which are in
this case already included in the specification, in the form of so-called
attributes of the addition operation. A third lemma is a kind of
"distributive law" between the successor operation and multiplication, and it
too is already included in the specification. Since this is just an
expository example, this is justified by the great familiarity and general
utility of these laws, but in general, lemmas should of course be proved
before they are used.
Another point is that we do not prove
- 1+ 2+ ... + n = n(n+1)/2
but instead we prove the equivalent formula
- sum(n) + sum(n) = n(n+1)
where sum(n) = 1+ 2+ ... + n. The
recursively defined operation sum is of
course needed to make precise the informal notation 1+
2+ ... + n, and the reformulation in terms of sum + sum is in order to avoid introducing the
division operation.
|
N
: Nat
)
sum(N) + sum(N) = N * (s N) .
