Email Gateway (Aug 18 2022 at 15:48): Email Gateway (Aug 18 2022 at 15:48):From: John Munroe <munddr@gmail.com>
Hi all,
Does anyone know how to prove
lemma "ALL (d1::real) d2 p q1 q2 k. (k > 1 & d1 > 0 & d2 > 0 & p > 0 &
q1 >= q2 & q2 > 0 & d1 < d2) --> ksqrt(q1p/d1) > ksqrt(q2p/d2)"
?
Even with the lemma:
lemma "ALL (d1::real) d2 p q1 q2. (d1 > 0 & d2 > 0 & p > 0 & q1 >= q2
& q2 > 0 & d1 < d2) --> sqrt(q1p/d1) > sqrt(q2p/d2)"
by (simp add: frac_less2 real_mult_order)
I can't seem to make use of it to prove the first. Sledgehammer helped
me prove the second, but it couldn't find anything for the first even
it looks like a rather straightforward extension of the second. Any
help will definitely be useful.
Thanks
John
Email Gateway (Aug 18 2022 at 15:49):From: Lawrence Paulson <lp15@cam.ac.uk>
Here is one possible approach:
lemma "ALL (d1::real) d2 p q1 q2 k. (k > 1 & d1 > 0 & d2 > 0 & p > 0 &
q1 >= q2 & q2 > 0 & d1 < d2) --> ksqrt(q1p/d1) > ksqrt(q2p/d2)"
apply (auto intro!: real_mult_less_mono2)
apply (metis frac_less2 real_mult_commute real_mult_le_cancel_iff2 real_mult_order)
done
The difficult part of this proof for sledgehammer is the inference from k>1 to k>0. Sledgehammer doesn't know anything about arithmetic and has to do everything from first principles.
Larry Paulson
Email Gateway (Aug 18 2022 at 15:49):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Donnerstag, den 12.08.2010, 23:28 +0100 schrieb John Munroe:
Hi all,
Does anyone know how to prove
lemma "ALL (d1::real) d2 p q1 q2 k. (k > 1 & d1 > 0 & d2 > 0 & p > 0 &
q1 >= q2 & q2 > 0 & d1 < d2) --> ksqrt(q1p/d1) > ksqrt(q2p/d2)"?
The goal is easy to solve directly just use C-c C-f to find the correct
lemmas:
First you want to remove the k, hence we search for: "?x * _ < ?x * <"
We find some introduction rules, but also the rewrite rule
mult_less_cancel_left (which is easier to handle).
The simplifier already rewrites "sqrt ?a < sqrt ?b" by "?a < ?b".
Now we have a division on a field, here we use the simp set:
field_simps
This results into: "q1 * d2 < q2 * d1"
This isn't handled by mult_less_cancel_left, however there are nice
introduction rules for this cases, just search for
"_ ==> _ * _ < _ * _"
and we find: mult_less_le_imp_less
hence the lemma is solved by:
lemma "ALL (d1::real) d2 p q1 q2 k. (k > 1 & d1 > 0 & d2 > 0 & p > 0 &
q1 >= q2 & q2 > 0 & d1 < d2) --> ksqrt(q1p/d1) > ksqrt(q2p/d2)"
by (auto simp: mult_less_cancel_left field_simps
intro: mult_less_le_imp_less)
You might add the introduction rule mult_less_le_imp_less with intro!
instead of just intro, this has the advantage to see the goals the auto
tactic can not solve, however it might apply the wrong rule and result
into an unprovable goal.
Greetings,
Even with the lemma:
lemma "ALL (d1::real) d2 p q1 q2. (d1 > 0 & d2 > 0 & p > 0 & q1 >= q2
& q2 > 0 & d1 < d2) --> sqrt(q1p/d1) > sqrt(q2p/d2)"
by (simp add: frac_less2 real_mult_order)I can't seem to make use of it to prove the first. Sledgehammer helped
me prove the second, but it couldn't find anything for the first even
it looks like a rather straightforward extension of the second. Any
help will definitely be useful.Thanks
John
Last updated: Apr 26 2024 at 16:20 UTC