Re: [isabelle] Proving lemmas containing a squareroot



On Fri, Jun 4, 2010 at 8:11 AM, Michael Daniels <dayzman at gmail.com> wrote:
> On Fri, Jun 4, 2010 at 3:36 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
>> Perhaps you meant "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" ?
>>
>
> Indeed, I've sent a follow-up about the typo but it hasn't reached the
> mailing list yet. What I meant is indeed EX rather than ALL. Any idea
> on what theorems should be used here and why sledgehammer fails to
> find any when it's sqrt?

If you are just interested in finding a proof, then here's one that works:

lemma exists_gt_conv_neq:
  fixes f :: "real => real"
  shows "(EX x y. f x > f y) = (EX x y. f x ~= f y)"
unfolding neq_iff by auto

lemma rt4: "EX a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt unfolding exists_gt_conv_neq by simp

But I think maybe your real question is why sledgehammer/metis are
having such trouble. One strategy you can try is to insert gt into the
subgoal before calling sledgehammer, instead of passing it via the
chained facts.

lemma rt4: "EX a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt
apply - (* this inserts axiom gt into the subgoal *)
sledgehammer;

Another thing you could do is realize that the only relevant property
of "sqrt(4)" is that it is positive. Sledgehammer and metis were able
to handle the following generalization:

lemma gt4': "0 < z ==> EX a b. z / pl a > z / pl b"
using gt apply -
sledgehammer;

Showing that "0 < sqrt(4)" is easy for the simplifier, but it requires
several extra rules to be passed to metis. (I think the numeral "4" is
actually a bigger problem than "sqrt".) The proof of the generalized
version gt4' is already rather difficult for metis (taking over a
minute on my machine), so I am not really surprised that the extra
complexity of "sqrt(4)" takes longer than you want to wait.

- Brian

>
> Thanks
> Michael
>
>> - Brian
>>
>





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