Re: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer



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/





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