[isabelle] sledgehammer issue

[Peter Lammich]

Hi Jasmin,

In Isabelle2016, I get the following weird sledgehammer output.

Sometimes, (I could not reproduce with small example), I also get the
message that e derived false from these facts, and that I should report
this as a "bug" in sledgehammer.


theory Scratch
imports Main 
  "$AFP/Refine_Monadic/Refine_Monadic"
begin


  lemma "A=B"
    using ASSERT_simps(1) inres_simps(3) pw_ASSERT(2)
    sledgehammer [provers = e]
(* Sledgehammering... 
"e": Try this: by metis (> 1.0 s, timed out).
*)
  oops    


--
  Peter

[Lawrence Paulson]

Sorry, what was that weird output? Do you mean this?

Post by Peter Lammich
Try this: by metis (> 1.0 s, timed out).

It looks normal to me. Sometimes proofs time out.

You can also get a warning if sledgehammer proves the goal without referring to the goal itself (specifically, its negation). This indicates that your assumptions are themselves inconsistent. Possibly too much use of"sorry". We all do it.

Larry

Post by Peter Lammich
Hi Jasmin,
In Isabelle2016, I get the following weird sledgehammer output.
Sometimes, (I could not reproduce with small example), I also get the
message that e derived false from these facts, and that I should report
this as a "bug" in sledgehammer.
theory Scratch
imports Main
"$AFP/Refine_Monadic/Refine_Monadic"
begin
lemma "A=B"
using ASSERT_simps(1) inres_simps(3) pw_ASSERT(2)
sledgehammer [provers = e]
(* Sledgehammering...
"e": Try this: by metis (> 1.0 s, timed out).
*)
oops
--
Peter

[Peter Lammich]

Post by Lawrence Paulson
Sorry, what was that weird output? Do you mean this?

Post by Peter Lammich
Try this: by metis (> 1.0 s, timed out).

This, in combination with the lemma "A=B", which is clearly not
provable (A,B are just variables). 

This indicates e found a proof for something unprovable. Btw, there
should be no "sorry"s in Main or "$AFP/Refine_Monadic/Refine_Monadic".

--
  Peter

Post by Lawrence Paulson
It looks normal to me. Sometimes proofs time out.
You can also get a warning if sledgehammer proves the goal without
referring to the goal itself (specifically, its negation). This
indicates that your assumptions are themselves inconsistent. Possibly
too much use of"sorry". We all do it.
Larry

Post by Peter Lammich
Hi Jasmin,
In Isabelle2016, I get the following weird sledgehammer output.
Sometimes, (I could not reproduce with small example), I also get the
message that e derived false from these facts, and that I should report
this as a "bug" in sledgehammer.
theory Scratch
imports Main 
  "$AFP/Refine_Monadic/Refine_Monadic"
begin
  lemma "A=B"
    using ASSERT_simps(1) inres_simps(3) pw_ASSERT(2)
    sledgehammer [provers = e]
(* Sledgehammering... 
"e": Try this: by metis (> 1.0 s, timed out).
*)
  oops    
--
  Peter

[Lawrence Paulson]

E 1.9.1 "Sungma" is the latest version of the successful automated
theorem prover.
Major user-visible improvements of E 1.9.1 are improved automatic
modes, automatic detection of input format, major fixes to the
watchlist mechanism (especially with respect to using it to provide
hints for proof search) and a bug-fix for a rarely triggered, but
nasty bug in clausification. We recommend all users of older versions
to upgrade to E 1.9.1.
You can find the source distribution and additional information at
the E website at
http://www.eprover.org

Larry

Post by Lawrence Paulson
Sorry, what was that weird output? Do you mean this?

Post by Peter Lammich
Try this: by metis (> 1.0 s, timed out).

This, in combination with the lemma "A=B", which is clearly not
provable (A,B are just variables).
This indicates e found a proof for something unprovable. Btw, there
should be no "sorry"s in Main or "$AFP/Refine_Monadic/Refine_Monadic".

[Peter Lammich]

A bug in E then.

If I understand it correctly, the bug could also be in the translation
from HOL to E, which is done by sledgehammer.

--
  Peter

If you are ambitious, you could try to isolate the input and see if
it yields a spurious proof when running E standalone. By coincidence,

E 1.9.1 "Sungma" is the latest version of the successful automated
theorem prover.
Major user-visible improvements of E 1.9.1 are improved automatic
modes, automatic detection of input format, major fixes to the
watchlist mechanism (especially with respect to using it to provide
hints for proof search) and a bug-fix for a rarely triggered, but
nasty bug in clausification. We recommend all users of older
versions
to upgrade to E 1.9.1.
You can find the source distribution and additional information at
the E website at
              http://www.eprover.org

Larry

Post by Lawrence Paulson
Sorry, what was that weird output? Do you mean this?

Post by Peter Lammich
Try this: by metis (> 1.0 s, timed out).

This, in combination with the lemma "A=B", which is clearly not
provable (A,B are just variables). 
This indicates e found a proof for something unprovable. Btw, there
should be no "sorry"s in Main or
"$AFP/Refine_Monadic/Refine_Monadic".

[Jasmin Blanchette]

Dear all,

Post by Peter Lammich

A bug in E then.

If I understand it correctly, the bug could also be in the translation
from HOL to E, which is done by sledgehammer.

I've just looked into it. As I suspected, the bug *is* in the translation from Isabelle/HOL to E. For those who are into arcane technicalities, this clause is clearly unsound:

fof(help_fequal_1_1_fequal_001t__Product____Type__Ounit_T, axiom,
((![X, Y]: ((~ pp(aa_Product_unit_bool(fequal_Product_unit(X), Y))) | X = Y)))).

There should be a predicate guarding "X" or "Y", as per the paper "Encoding Monomorphic and Polymorphic Types". I can repair this.

Cheers,

Jasmin

[Dmitriy Traytel]

Hi Larry,

I very much hope that the AFP editors have ensured that “sorry" is not used in AFP entries (which is the only imported thing in Peter’s example next to Main).

Dmitriy

Post by Lawrence Paulson
Sorry, what was that weird output? Do you mean this?

Post by Peter Lammich
Try this: by metis (> 1.0 s, timed out).

It looks normal to me. Sometimes proofs time out.
You can also get a warning if sledgehammer proves the goal without referring to the goal itself (specifically, its negation). This indicates that your assumptions are themselves inconsistent. Possibly too much use of"sorry". We all do it.
Larry

Post by Peter Lammich
Hi Jasmin,
In Isabelle2016, I get the following weird sledgehammer output.
Sometimes, (I could not reproduce with small example), I also get the
message that e derived false from these facts, and that I should report
this as a "bug" in sledgehammer.
theory Scratch
imports Main
"$AFP/Refine_Monadic/Refine_Monadic"
begin
lemma "A=B"
using ASSERT_simps(1) inres_simps(3) pw_ASSERT(2)
sledgehammer [provers = e]
(* Sledgehammering...
"e": Try this: by metis (> 1.0 s, timed out).
*)
oops
--
Peter