It seems doesn't work. Could you please explain it in detail?
-Original Messages-
From:"Ramana Kumar"
Sent Time:2017-10-23 05:38:07 (Monday)
To: "Liu Gengyang" <2015200...@mail.buct.edu.cn>
Cc: hol4_QA
Subject: Re: [Hol-info] Small question about sqrt
I
Thanks, I think that's the reason, too.
-Original Messages-
From:michael.norr...@data61.csiro.au
Sent Time:2017-10-23 07:17:02 (Monday)
To: hol-info@lists.sourceforge.net
Cc:
Subject: Re: [Hol-info] Small question about sqrt
Square root is unspecified on numbers < 0, so you do
Square root is unspecified on numbers < 0, so you don’t know that there is not
a negative number whose square root is 0.
Michael
From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Saturday, 21 October 2017 at 00:05
To: hol4_QA
Subject: [Hol-info] Small question about sqrt
Hi,
In your first goal, do either of these work?
metis_tac[transcTheory.SQRT_0]
rw[] \\ imp_res_tac transcTheory.SQRT_0
On 20 October 2017 at 23:42, Liu Gengyang <2015200...@mail.buct.edu.cn>
wrote:
> Hi,
>
> I want to prove the goal: !x. (sqrt x = 0) ==> (x = 0) as below,
>
> RW_TAC realLib.real_s
Hi,
I want to prove the goal: !x. (sqrt x = 0) ==> (x = 0) as below,
RW_TAC realLib.real_ss [] >>
`sqrt 0 = 0` by RW_TAC realLib.real_ss [transcTheory.SQRT_0]
The result is:
x = 0
0. sqrt x = 0
1. sqrt 0 = 0
I think it is obvious, but I can'n prove
