[isabelle] metis -unused theorems

[Dr A. Koutsoukou-Argyraki]

Dear Isabelle users,

I have the following question which is not an actual problem, but I am
just wondering
why metis behaves this way:

the following keeps happening:
sledgehammer gives one (or more) proof(s) by metis,
but when I apply the suggested proof, I get the output message "unused
theorems"

(When this happens afterwards either I delete the named unused theorems,
or use
(some of) them to help sledgehammer to give me another simpler proof.)

I just find this metis behaviour a bit puzzling -any insight?

Thanks a lot,
Best wishes,
Angeliki

[Jasmin Blanchette]

Dear Angeliki,

Post by Dr A. Koutsoukou-Argyraki
sledgehammer gives one (or more) proof(s) by metis,
but when I apply the suggested proof, I get the output message "unused theorems"
[...]
I just find this metis behaviour a bit puzzling -any insight?

It is hard to tell without a concrete example, but a possible explanation is that Sledgehammer includes a minimization phase, described in e.g. Section 6.6.5 of my thesis:

https://mediatum.ub.tum.de/doc/1097834/1097834.pdf <https://mediatum.ub.tum.de/doc/1097834/1097834.pdf>

However, since proof search in FOL is not a decision procedure, we have to use a time limit when invoking the prover for minimizing. Hence as a result, we lose any guarantees that the minimized result is minimal.

In the file src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML, on line 129, you will find this constant:

val slack_msecs = 200

You could try increasing it to, e.g., 2000 and see if it has an impact. There's of course a tradeoff between fast minimization and "minimal" minimization. It seems like it's hard to get both.

Cheers,

Jasmin

[Dr A. Koutsoukou-Argyraki]

Dear Jasmin,

thanks a lot for your answer.

Post by Jasmin Blanchette
In the file
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML, on line
val slack_msecs = 200
You could try increasing it to, e.g., 2000 and see if it has an
impact. There's of course a tradeoff between fast minimization and
"minimal" minimization. It seems like it's hard to get both.

I tried what you suggested and (even though I haven't retried my
previous proofs yet)
I now also see that several such output messages appear by metis wrt
"unused theorems"
even in theories in the Analysis library, e.g.in the theory
Arcwise.Connected.thy lines 1243 1957.
On line 1243 metis says: unused theorems: a_ge_0 b_le_1 but if one
tries to remove them, the proof doesn't work! (which might be a bug(?))
On line 1957 metis says unused theorems: "??.unknown",
"Path_Connected.arc_imp_path".
By removing the latter, the proof works.
(Disclaimer: I haven't pushed any such changes in the library theories!)

In my own proofs whenever I got this message by metis the proof always
worked after removing the superfluous theorems.

As mentioned before, it's not a problem in praxis, it's interesting
though to find the cause of this.

Thanks again,
Best,
Angeliki

Post by Jasmin Blanchette
Dear Angeliki,

Post by Dr A. Koutsoukou-Argyraki
sledgehammer gives one (or more) proof(s) by metis,
but when I apply the suggested proof, I get the output message "unused theorems"
[...]
I just find this metis behaviour a bit puzzling -any insight?

It is hard to tell without a concrete example, but a possible
explanation is that Sledgehammer includes a minimization phase,
https://mediatum.ub.tum.de/doc/1097834/1097834.pdf [1]
However, since proof search in FOL is not a decision procedure, we
have to use a time limit when invoking the prover for minimizing.
Hence as a result, we lose any guarantees that the minimized result is
minimal.
In the file
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML, on line
val slack_msecs = 200
You could try increasing it to, e.g., 2000 and see if it has an
impact. There's of course a tradeoff between fast minimization and
"minimal" minimization. It seems like it's hard to get both.
Cheers,
Jasmin
------
[1] https://mediatum.ub.tum.de/doc/1097834/1097834.pdf

[Christian Sternagel]

Dear Angeliki,

just an experience report.

I regularly encounter these "unused theorems" warnings you are talking
about.

However, I would not blindly remove such unused theorems, since in my
experience it is often the case that the corresponding metis proof will
be quite a bit slower after that.

cheers

chris

Post by Dr A. Koutsoukou-Argyraki
Dear Jasmin,
thanks a lot for your answer.

Post by Jasmin Blanchette
In the file
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML, on line
 val slack_msecs = 200
You could try increasing it to, e.g., 2000 and see if it has an
impact. There's of course a tradeoff between fast minimization and
"minimal" minimization. It seems like it's hard to get both.

I tried what you suggested and (even though I haven't retried my
previous proofs yet)
I now also see that several such output messages appear by metis wrt
"unused theorems"
even in theories in the Analysis library, e.g.in the theory
Arcwise.Connected.thy  lines 1243 1957.
On line 1243 metis says: unused theorems:  a_ge_0 b_le_1 but if one
tries to remove them, the proof doesn't work! (which might be a bug(?))
On line 1957 metis says unused theorems: "??.unknown",
"Path_Connected.arc_imp_path".
By removing the latter, the proof works.
(Disclaimer: I haven't pushed any such changes in the library theories!)
In my own proofs whenever I got this message  by metis the proof always
worked after removing the superfluous theorems.
As mentioned before, it's not a problem in praxis, it's interesting
though to find the cause of this.
Thanks again,
Best,
Angeliki

Post by Jasmin Blanchette
Dear Angeliki,

Post by Dr A. Koutsoukou-Argyraki
sledgehammer gives one (or more) proof(s) by metis,
but when I apply the suggested proof, I get the output message "unused theorems"
[...]
I just find this metis behaviour a bit puzzling -any insight?

It is hard to tell without a concrete example, but a possible
explanation is that Sledgehammer includes a minimization phase,
 https://mediatum.ub.tum.de/doc/1097834/1097834.pdf [1]
However, since proof search in FOL is not a decision procedure, we
have to use a time limit when invoking the prover for minimizing.
Hence as a result, we lose any guarantees that the minimized result is
minimal.
In the file
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML, on line
 val slack_msecs = 200
You could try increasing it to, e.g., 2000 and see if it has an
impact. There's of course a tradeoff between fast minimization and
"minimal" minimization. It seems like it's hard to get both.
Cheers,
Jasmin
------
[1] https://mediatum.ub.tum.de/doc/1097834/1097834.pdf

[Dominique Unruh]

Hi,

However, I would not blindly remove such unused theorems, since in my

Post by Christian Sternagel
experience it is often the case that the corresponding metis proof will
be quite a bit slower after that.

if that is indeed the case, perhaps the warning should be changed into a
"tracing" message?
Because as I understand warnings, they are things that should be fixed (and
I usually try to get all warnings out of my code).
So having metis output a warning "forces" me to remove extra theorems (or
to change my coding style).

Best wishes,
Dominique.

Post by Christian Sternagel
Dear Angeliki,
just an experience report.
I regularly encounter these "unused theorems" warnings you are talking
about.
However, I would not blindly remove such unused theorems, since in my
experience it is often the case that the corresponding metis proof will
be quite a bit slower after that.
cheers
chris

Post by Dr A. Koutsoukou-Argyraki
Dear Jasmin,
thanks a lot for your answer.

Post by Jasmin Blanchette
In the file
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML, on line
val slack_msecs = 200
You could try increasing it to, e.g., 2000 and see if it has an
impact. There's of course a tradeoff between fast minimization and
"minimal" minimization. It seems like it's hard to get both.

I tried what you suggested and (even though I haven't retried my
previous proofs yet)
I now also see that several such output messages appear by metis wrt
"unused theorems"
even in theories in the Analysis library, e.g.in the theory
Arcwise.Connected.thy lines 1243 1957.
On line 1243 metis says: unused theorems: a_ge_0 b_le_1 but if one
tries to remove them, the proof doesn't work! (which might be a bug(?))
On line 1957 metis says unused theorems: "??.unknown",
"Path_Connected.arc_imp_path".
By removing the latter, the proof works.
(Disclaimer: I haven't pushed any such changes in the library theories!)
In my own proofs whenever I got this message by metis the proof always
worked after removing the superfluous theorems.
As mentioned before, it's not a problem in praxis, it's interesting
though to find the cause of this.
Thanks again,
Best,
Angeliki

Post by Jasmin Blanchette
Dear Angeliki,

Post by Dr A. Koutsoukou-Argyraki
sledgehammer gives one (or more) proof(s) by metis,
but when I apply the suggested proof, I get the output message "unused theorems"
[...]
I just find this metis behaviour a bit puzzling -any insight?

It is hard to tell without a concrete example, but a possible
explanation is that Sledgehammer includes a minimization phase,
https://mediatum.ub.tum.de/doc/1097834/1097834.pdf [1]
However, since proof search in FOL is not a decision procedure, we
have to use a time limit when invoking the prover for minimizing.
Hence as a result, we lose any guarantees that the minimized result is
minimal.
In the file
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML, on line
val slack_msecs = 200
You could try increasing it to, e.g., 2000 and see if it has an
impact. There's of course a tradeoff between fast minimization and
"minimal" minimization. It seems like it's hard to get both.
Cheers,
Jasmin
------
[1] https://mediatum.ub.tum.de/doc/1097834/1097834.pdf