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 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 <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Small question about sqrt
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 it by rewrite or simplify tactic.
However, if the goal is: !x. x>=0 /\ (sqrt x = 0) ==> (x = 0), I can prove it
as below:
RW_TAC std_ss [] >>
`sqrt x pow 2 = 0 pow 2` by RW_TAC std_ss [] >>
`0 <= x` by RW_TAC std_ss [realTheory.real_ge] >-
RW_TAC std_ss [GSYM realTheory.real_ge] >>
FULL_SIMP_TAC realLib.real_ss [transcTheory.SQRT_POW_2]
So, what the problem about the first goal?
Regards，
Liu
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
