*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer*From*: Christoph LANGE <math.semantic.web at gmail.com>*Date*: Sun, 27 Oct 2013 16:09:11 +0100*In-reply-to*: <526D2BE8.1010801@gmail.com>*Organization*: University of Birmingham*References*: <526D2BE8.1010801@gmail.com>*Sender*: Christoph Lange <allegristas at gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130919 Thunderbird/17.0.9

A minor correction: 2013-10-27 16:06 Christoph LANGE: > my impression (which may have been wrong) from Isabelle2013 was that > "try" tries "try0" before "sledgehammer". In Isabelle2013-1-RC3 this no > longer seems to be the case. > > I find this quite annoying because I have made it a habit to enter "try" > after almost every statement. In many cases I don't know whether try0 > would be sufficient to prove something, or whether a more complex proof > (such as those that sledgehammer finds) is required. Then, when > sledgehammer finds a proof, looking at the lemmas used by this proof > sometimes gives me the intuition that try0 might also suffice, e.g. when > I know that all of these lemmas are simp rules. > > Here is a self-contained almost minimal example. I didn't try this with > older versions but I'd be happy to do so. Please ignore the first step: > maybe there is an easier proof for this, but for _this_ email only the > second step is relevant. OK, I see this is not the most elegant example, as … > > notepad > begin > fix R::"('a × 'b) set" > and N::"'a set" > and n::'a > have "{ (x, y) . (x, y) ∈ R ∧ x ≠ n }¯ = { (y, x) . (y, x) ∈ R¯ ∧ x ≠ n }" > by (smt Collect_cong converse_unfold curryE curry_split > mem_Collect_eq splitD split_cong) > then have "Domain { (x, y) . (x, y) ∈ R ∧ x ≠ n } = Range { (y, x) . > (y, x) ∈ R¯ ∧ x ≠ n}" try > end > > On my machine try0 finds that simp/auto/force each take 2 ms. > > However when I say "try", it resorts to running sledgehammer, which > tells me: > > --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- > Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and > "nitpick"... > "z3": Sledgehammer ("z3") found a proof: by (metis Range_converse) (128 ms). > To minimize: sledgehammer min (Range_converse `{(x, y). (x, y) ∈ R ∧ x ≠ > n}¯ = {(y, x). (y, x) ∈ R¯ ∧ x ≠ n}`). > "spass": Sledgehammer ("spass") found a proof: by (metis Range_converse) > (108 ms). > To minimize: sledgehammer min (Range_converse `{(x, y). (x, y) ∈ R ∧ x ≠ > n}¯ = {(y, x). (y, x) ∈ R¯ ∧ x ≠ n}`). > "remote_vampire": Sledgehammer ("remote_vampire") found a proof: by > (metis Range_converse converse_unfold) (109 ms). > To minimize: sledgehammer min (Range_converse converse_unfold `{(x, y). > (x, y) ∈ R ∧ x ≠ n}¯ = {(y, x). (y, x) ∈ R¯ ∧ x ≠ n}`). > "e": Sledgehammer ("e") found a proof: by (smt Collect_mem_eq > Domain_Collect_split Domain_converse Domain_unfold converse_converse > converse_unfold internal_split_def) (28 ms). > To minimize: sledgehammer min [smt] (Collect_mem_eq Domain_Collect_split > Domain_converse Domain_unfold converse_converse converse_unfold > internal_split_def `{(x, y). (x, y) ∈ R ∧ x ≠ n}¯ = {(y, x). (y, x) ∈ R¯ > ∧ x ≠ n}`). > Structured proof (3 ms): > proof - > show "Domain {(x, y). (x, y) ∈ R ∧ x ≠ n} = Range {(y, x). (y, x) ∈ R¯ > ∧ x ≠ n}" > using Domain_unfold by auto > qed … this shows that the first proof step is not necessary at all, because "using Domain_unfold by auto" suffices to establish the second step without the first step. Still this doesn't affect my point that "try" seems to give preference to "sledgehammer" over "try0". > --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- > > Here, it was clearly the last sledgehammer output that gave me the idea > that try0 can do the job. In other cases (I'll be happy to dig out some > more) it's not that easy. > > Any ideas? > > Cheers, and thanks in advance, > > Christoph > -- Christoph Lange, School of Computer Science, University of Birmingham http://cs.bham.ac.uk/~langec/, Skype duke4701 → Mathematics in Computer Science Special Issue on “Enabling Domain Experts to use Formalised Reasoning”; submission until 31 October. http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/

**References**:

- Previous by Date: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer
- Next by Date: Re: [isabelle] [Isabelle2013-1 RC] Scalability problem with re-entrant build of the whole distribution
- Previous by Thread: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer
- Next by Thread: [isabelle] WRLA 2014 Call for papers
- Cl-isabelle-users October 2013 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