I am trying to prove the following sum: 1^3 + 2^3 + 3^3 .. n^3 = (n^2 (n+1)^2) / 4
I have made the following function for the left side val sum_cube_def = Define `(sum_cube 0 = 0) /\ (sum_cube(SUC n) = (&(n+1) pow 3)+sum_cube n)`; and a goal that I am trying to prove now g `!n. sum_cube_def n = (((&n) pow 2)*(&(n+1)) pow 2)/4`; I plan on proving the above by induction, first for n=0 then for n+1. I have simplified the above subgoal after applying Induct_on `n` and applying the following e(REWRITE_TAC [POW_2]);e(REWRITE_TAC [REAL_MUL_LZERO]);e(REWRITE_TAC [real_div]);e(REWRITE_TAC [REAL_MUL_LZERO]); Currently I am stuck with the following : `sum_cube_def 0 = 0` I was expecting HOL to give me a Goal Proved message by now since 0 = 0, but it doesn't. I have tried . e(RW_TAC std_ss[sum_cube_def]); and e(RW_TAC std_ss[]); but to no avail. Can anyone help me out with this and tell me How can I explain a 0 = 0 to HOL? ------------------------------------------------------------------------------ The best possible search technologies are now affordable for all companies. Download your FREE open source Enterprise Search Engine today! Our experts will assist you in its installation for $59/mo, no commitment. Test it for FREE on our Cloud platform anytime! http://pubads.g.doubleclick.net/gampad/clk?id=145328191&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
