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
