Hi,
I want to prove the goal:
!a b c d.(sqrt(c pow 2 + d pow 2) pow 2 = c pow 2 + d pow 2) /\ (sqrt(a pow 2 +
b pow 2) pow 2 = a pow 2 + b pow 2) /\ sqrt(c pow 2 + d pow 2) pow 2 ≤ sqrt(a
pow 2 + b pow 2) pow 2 ==> c pow 2 + d pow 2 ≤ a pow 2 + b pow 2
In theory this goal can be proved by FULL_SIMP_TAC, but failed. However, the
goal as below who have the same structure can be proved by FULL_SIMP_TAC.
!a b c d e f.(a = b + e) /\ (c = d + f) /\ a <= c ==> b + e <= d + f
What's the problem with the first goal, how can I prove it?
P.S. The origin goal is:
!a b c d.sqrt(a pow 2 + b pow 2) >= sqrt(c pow 2 + d pow 2) ==> a * a + b * b
>= c * c + d * d
RW_TAC std_ss [] >>
`0 <= c pow 2 + d pow 2` by RW_TAC std_ss
[realTheory.REAL_LE_POW2,realTheory.REAL_LE_ADD] >>
`0 <= a pow 2 + b pow 2` by RW_TAC std_ss
[realTheory.REAL_LE_POW2,realTheory.REAL_LE_ADD] >>
`0 <= sqrt (c pow 2 + d pow 2)` by RW_TAC std_ss [transcTheory.SQRT_POS_LE] >>
`0 <= sqrt (a pow 2 + b pow 2)` by RW_TAC std_ss [transcTheory.SQRT_POS_LE] >>
`sqrt (c pow 2 + d pow 2) pow 2 <= sqrt (a pow 2 + b pow 2) pow 2` by
FULL_SIMP_TAC std_ss [realTheory.real_ge,realTheory.POW_LE] >>
FULL_SIMP_TAC std_ss [GSYM transcTheory.SQRT_POW2] >>(*Here is the problem.*)
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
