Re: [isabelle] Comparing square roots



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


> 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.