On 4/4/14, Warren D Smith <warren.wds@gmail.com> wrote:
Here is a sketch of how to prove the knight distance formula using MAPLE9. I am not going to prove it, I am merely going to explain how somebody better than I with symbolic manip programs, could prove it. ...
This looked an interesting idea, and I tinkered with it for a while to see if it could be persuaded to work under Maple 17. My version 1 is essentially identical to WDS' first attempt, except for assuming integers and attaching special case x = y = 0 to his function g . The impressively messy result looks nothing like WDS' expression starting g(x,y) = max(| x |, | y |) - min(| x |, | y |) - 2 floor(1/4 max(| x |, | y |) - ... --- however both deliver incorrect test results for some arguments! Version 2 restricts the region to x > y > 1 . The result is considerably shorter, and tests correct for all arguments --- both in the region and outside! Version 3 omits all special cases from both f and g definitions. The result (unsurprisingly) still tests incorrect --- but (remarkably) is now identical to WDS' original above! Version 4 again restricts the region to x > y > 1 . The result is much shorter again than any previous --- and despite the incorrect definitions, tests correct for all arguments! I get g(x, y) = 1 for |x|,|y| <= 10 , where g(x, y) := x-y-2*floor((1/4)*x-(1/2)*y) - min( max(x-2, y+1)-min(x-2, y+1)-2*floor((1/4)*max(x-2, y+1)-(1/2)*min(x-2, y+1)), max(x-1, y+2)-min(x-1, y+2)-2*floor((1/4)*max(x-1, y+2)-(1/2)*min(x-1, y+2)), x-y-2*floor((1/4)*x-(1/2)*y)-1, x+1-y-2*floor((1/4)*x+1/4-(1/2)*y), x+1-y-2*floor((1/4)*x+3/4-(1/2)*y) ); This sadly predictable muddle confirms my suspicion that the project is ahead of the technology available to implement it, which will come as no surprise to anyone who recalls my posts on failing to prove automatically theorems about binomial coefficients. It might perhaps be worth another attempt under Mathematica or Macsyma --- but I'm not holding my breath!
OK? So I hope I've made it clear (a) exactly how to prove this now (b) Lunnon should see what is inadequate about his "proof", (c) what is inadequate about MAPLE9 simplifier ... this whole proof would have been a triviality if it had a good simplifier.
As I have observed on a previous occasion: if my proof is claimed incorrect, I would be much obliged to be informed where the error is believed to occur. Fred Lunnon