Hi Liu,
rewriting applies the provided equations left to write. So if if have
(A = A') /\ (B = B') ==> (f A B)
The simplifier (with std_ss) uses the precondition (A = A') /\ (B = B')
as context and adds the rewrite rules
A -> A'
B -> B'
where "->" is an ad-hoc notation for "=" but only applied in this
direction. It then uses these rules to rewrite
f A B
to
f A' B'.
So, for your example:
``!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``
the equations are in the wrong direction to be used as rewrites for the
conclusion. They could be used on the 3rd conjunct (which you probably
expected). However, the 3rd conjunct is not simplified with the other
conjuncts. They are not used as context by std_ss. So, if you write
``!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``
(notice /\ replaced by ==>) it works and is semantically equivalent.
Your simplified example
!a b c d e f. (a = b + e) /\ (c = d + f) /\ a <= c ==> b + e <= d + f
works, because a and c are quantified variables, which are removed by
quantifier instantiation. If you strip away the quantifiers, it stops
working.
I recommend using STRIP_TAC and REV_FULL_SIMP_TAC.
Cheers
Thomas
On 09.11.2017 04:02, Liu Gengyang wrote:
> 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
------------------------------------------------------------------------------
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
