Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] sledgehammer issue

view this post on Zulip Email Gateway (Aug 22 2022 at 13:53):

From: Peter Lammich <lammich@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:03):

From: Lawrence Paulson <lp15@cam.ac.uk>
Sorry, what was that weird output? Do you mean this?

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

On 31 Aug 2016, at 16:08, Peter Lammich <lammich@in.tum.de> wrote:

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:04):

From: Peter Lammich <lammich@in.tum.de>
On Do, 2016-09-01 at 12:36 +0100, Lawrence Paulson wrote:

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

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:05):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:06):

From: Lawrence Paulson <lp15@cam.ac.uk>
A bug in E then. 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, a new version was released yesterday, warning of a bug:

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

On 1 Sep 2016, at 12:50, Peter Lammich <lammich@in.tum.de> wrote:

On Do, 2016-09-01 at 12:36 +0100, Lawrence Paulson wrote:

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

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:07):

From: Peter Lammich <lammich@in.tum.de>
On Do, 2016-09-01 at 13:03 +0100, Lawrence Paulson wrote:

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.

view this post on Zulip Email Gateway (Aug 22 2022 at 14:08):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear all,

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

Last updated: Apr 16 2024 at 20:15 UTC