The name of the constant you defined is "sum_cube", not "sum_cube_def" as
in your goal.
On Sat, May 24, 2014 at 10:58 AM, Valerie Martin <[email protected]> wrote:
> 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
>
------------------------------------------------------------------------------
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
