On 10 Nov 2009, at 05:52, Curt Sampson wrote:
On 2009-11-09 14:22 -0800 (Mon), muad wrote:
Proof: True for n = 0, 1, 2, 3, 4 (check!), hence true for all n. QED. ...
Actually, the test is that it's true for 0 through 4 is not sufficient for a proof;
It's enough testing...
you also need to prove in some way that you need do no further tests.
...and you can calculate how much testing is enough by computing an upper bound on the polynomial degree of the expression. (The summation operator increments degree, the difference operator decreases it, like in calculus.)
Showing that particular point in this case appears to me to lie outside the realm of testing.
You need to appeal to a general theorem about expressions of a particular form, but if that theorem is in the library, the only work you need do is to put the expressions in that form. This is sometimes described as the "reflective" proof method: express problem in language capturing decidable fragment; hit with big stick. There are lots of other examples of this phenomenon. The zero-one principle for sorting networks is a favourite of mine. I'm sure there's more to be found here. It smells a bit of theorems for free: the strength comes from knowing what you don't. All the best Conor