*To*: Michael Daniels <dayzman at gmail.com>*Subject*: Re: [isabelle] Proving lemmas containing a squareroot*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 4 Jun 2010 10:07:13 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTim7wPVyqwnxdcCZUpmiVlUwFsYxgo7W5ESauSdT@mail.gmail.com>*References*: <AANLkTintDKxYCcQNGUIuYAANd65eAdQqmnHc4SMyMpf5@mail.gmail.com> <AANLkTiniOn8v0hcKkMc4nllmMtDuVXWGQW1Ci84X_7DL@mail.gmail.com> <AANLkTim7wPVyqwnxdcCZUpmiVlUwFsYxgo7W5ESauSdT@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Proving lemmas containing a squareroot***From:*Michael Daniels

**References**:**[isabelle] Proving lemmas containing a squareroot***From:*Michael Daniels

**Re: [isabelle] Proving lemmas containing a squareroot***From:*Brian Huffman

**Re: [isabelle] Proving lemmas containing a squareroot***From:*Michael Daniels

- Previous by Date: Re: [isabelle] Proving lemmas containing a squareroot
- Next by Date: Re: [isabelle] Implicit typing in lemma
- Previous by Thread: Re: [isabelle] Proving lemmas containing a squareroot
- Next by Thread: Re: [isabelle] Proving lemmas containing a squareroot
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list