Discussion:
[isabelle] sledgehammer issue
(too old to reply)
Peter Lammich
2016-08-31 15:11:30 UTC
Permalink
Raw Message
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
2016-09-01 11:44:17 UTC
Permalink
Raw Message
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
2016-09-01 11:55:59 UTC
Permalink
Raw Message
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
2016-09-01 12:08:25 UTC
Permalink
Raw Message
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
2016-09-01 13:46:29 UTC
Permalink
Raw Message
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
2016-09-01 13:57:03 UTC
Permalink
Raw Message
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
2016-09-01 12:00:26 UTC
Permalink
Raw Message
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
Loading...