Hi,
Your goal is wrong somehow. You used "sum_cube_def" which is a name of
the definition but not the function which is "sum_cube"
GOAL:
g `!n. sum_cube n = (((&n) pow 2)*(&(n+1)) pow 2)/4`;
Following will prove the base case:
e(Induct_on `n`);;
e(RW_TAC real_ss[sum_cube_def]);;
--Umair
> Message: 5
> Date: Sat, 24 May 2014 14:58:39 +0500
> From: Valerie Martin <recho...@gmail.com>
> Subject: [Hol-info] Stuck in trying to prove a simple mathematical
> summation
> To: hol-info@lists.sourceforge.net
> Message-ID:
> <CA+igsXWqRPwHjXhOCdWy7iah7Mgpgh+2Lz4r=
> 3cz1jr1gs-...@mail.gmail.com>
> Content-Type: text/plain; charset=UTF-8
>
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> End of hol-info Digest, Vol 96, Issue 8
> ***************************************
>
>
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
