Re: [isabelle] Comparing square roots



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) --> k*sqrt(q1*p/d1) > k*sqrt(q2*p/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


On 12 Aug 2010, at 23:28, John Munroe wrote:

> 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) --> k*sqrt(q1*p/d1) > k*sqrt(q2*p/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(q1*p/d1) > sqrt(q2*p/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
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.