Tony Johnson wrote:
> How would I go about proving something simple like this?
> 1 + 2 + 3 + \dots + n = \frac{n(n+1)}{2}
First you need to define your summation.
Life is usually easiest if you define things by pattern-matching
recursion:
val sum_def = Define`
(sum 0 = 0) /\
(sum (SUC n) = SUC n + sum n)
`;
Such a definition is a prime candidate for automatic rewriting, so I
would then add the definition to the built-in simpset
val _ = export_rewrites ["sum_def"]
Then you get to state your theorem. Proving things with DIV is
usually a pain, so I recast by multiplying both sides by two:
val sum_form = store_thm(
"sum_form",
``2 * sum n = n * (n + 1)``,
<tactic>)
What's the <tactic>? First an induction
Induct_on `n` THEN ...
Following induction steps by rewriting is usually safe, so
Induct_on `n` THEN SRW_TAC [][]
This eliminates the base case automatically and gives the goal
2 * (SUC n + sum n) = SUC n * (SUC n + 1)
-------------------------------------------
2 * sum n = n * (n + 1)
where the formula below the line is the inductive hypothesis.
The IH would apply as a rewrite if the multiplication had been pushed
into the addition. This is the theorem
arithmeticTheory.LEFT_ADD_DISTRIB. Let's assume you have done an
open arithmeticTheory
so that we don't have to use fully-qualified names everywhere.
Then, we can modify our tactic to be
Induct_on `n` THEN SRW_TAC [][LEFT_ADD_DISTRIB] THEN ...
This gives
2 * SUC n + (n * n + n) = SUC n * SUC n + SUC n
-------------------------------------------------
2 * sum n = n * (n + 1)
The IH has been applied and now our goal is pure arithmetic. As it
stands it is not a useful instance of a Presburger formula because of
the n * n and the SUC n * SUC n. But the latter can be expanded to a
formula including the former with the use of the standard
MULT_CLAUSES, which includes the conjuncts
|- SUC n * m = n * m + m
|- n * SUC m = n + n * m
So, we modify the tactic to be
Induct_on `n` THEN SRW_TAC [][LEFT_ADD_DISTRIB, MULT_CLAUSES] THEN
...
This gives a goal of
2 + 2 * n + (n * n + n) = n + n * n + (SUC n + 1)
---------------------------------------------------
2 * sum n = n * (n + 1)
This is now a good instance of a Presburger formula (with n*n
substituted out for an arbitrary variable), meaning that DECIDE_TAC
will solve it.
So our final tactic is
Induct_on `n` THEN SRW_TAC [][LEFT_ADD_DISTRIB, MULT_CLAUSES] THEN
DECIDE_TAC
and the final proof looks like
val sum_form = store_thm(
"sum_form",
``2 * sum n = n * (n + 1)``,
Induct_on `n` THEN SRW_TAC [][LEFT_ADD_DISTRIB, MULT_CLAUSES] THEN
DECIDE_TAC)
The form with division can subsequently be done (in a slightly hacky way) as
val sum_form_div = store_thm(
"sum_form_div",
``sum n = n * (n + 1) DIV 2``,
SRW_TAC [][Once EQ_SYM_EQ] THEN MATCH_MP_TAC DIV_UNIQUE THEN
Q.EXISTS_TAC `0` THEN SRW_TAC [][GSYM sum_form, MULT_COMM]);
Michael.
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
