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
