It seems doesn't work. Could you please explain it in detail?
-----Original Messages-----
From:"Ramana Kumar" <ramana.ku...@cl.cam.ac.uk>
Sent Time:2017-10-23 05:38:07 (Monday)
To: "Liu Gengyang" <2015200...@mail.buct.edu.cn>
Cc: hol4_QA <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Small question about sqrt
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_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
------------------------------------------------------------------------------
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
