Thank you very much,its works!
-----Original Messages-----
From:michael.norr...@data61.csiro.au
Sent Time:2017-11-09 11:15:52 (Thursday)
To: 2015200...@mail.buct.edu.cn
Cc:
Subject: Re: [Hol-info] A problem of derivation
Use the theorem SQRT_POW_2. E.g.:
Q.prove(
`!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`,
simp[transcTheory.SQRT_POW_2, realTheory.REAL_LE_POW2,
realTheory.REAL_LE_ADD]);
Michael
From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Thursday, 9 November 2017 at 14:07
To: hol4_QA <hol-info@lists.sourceforge.net>
Subject: [Hol-info] A problem of derivation
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
