Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] very slow metis proofs: is that an issue?

view this post on Zulip Email Gateway (Aug 12 2025 at 19:36):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Hello,

today I happened to compile "HOL-Analysis.Abstract_Topological_Spaces"
which takes about 5 minutes on my notebook.
Out of curiosity, I looked at the longest "by metis" which takes about
20 s. It is

by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin
continuous_map_closedin)

on line 3310.

A trivial transformation (guessed easily without understanding what is
going on in the proof) to

using closed_real_atLeastAtMost[unfolded closed_closedin]
assms[unfolded continuous_map_closedin]  by blast

brings it down to practically zero.

This is not very interesting in itself but it raises for me following
questions:

Stepan

view this post on Zulip Email Gateway (Aug 13 2025 at 07:25):

From: Martin Desharnais <martin.desharnais@posteo.de>
Hi Stepan,

On 12.08.25 21:28, Stepan Holub (via cl-isabelle-users Mailing List) wrote:

Out of curiosity, I looked at the longest "by metis" which takes about
20 s. It is

by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin
continuous_map_closedin)

on line 3310.

A trivial transformation (guessed easily without understanding what is
going on in the proof) to

using closed_real_atLeastAtMost[unfolded closed_closedin]
assms[unfolded continuous_map_closedin]  by blast

brings it down to practically zero.

I checked the mentioned theory and found two duplicates of the proof you
presented, each of which taking approximately 7.5 seconds on my laptop.
I (very slightly) generalized the proof step, proved it with your
suggested proof, and reused the generalized proof step in both places
(See Isabelle/7ac70210d12c).

This is not very interesting in itself but it raises for me following
questions:

I suspect that many the verification of many formalizations could be
sped up by tuning some of the proofs.

As for caring about it, opinions may vary. I believe that one should
strive for a balance between readability, maintainability, and
verification performance; verification performance not only reduce the
running time, but also the energy consumption.

I believe the change you proposed was a good one, because it improved
both readability and performance.

Yes, some proof refactoring could be automated if one was to invest the
time into writing a tool. Many heuristics could be used including AI,
Sledgehammer, try0, and metis_instantiate. I personally like to use
metis_instantiate and select some simple fact instantiation that
simplify the proof search.

Regards,
Martin

view this post on Zulip Email Gateway (Aug 13 2025 at 07:29):

From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Stepan Holub wrote:

today I happened to compile "HOL-Analysis.Abstract_Topological_Spaces"
which takes about 5 minutes on my notebook.
Out of curiosity, I looked at the longest "by metis" which takes about
20 s. It is

by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin
continuous_map_closedin)

on line 3310.

A trivial transformation (guessed easily without understanding what is
going on in the proof) to

using closed_real_atLeastAtMost[unfolded closed_closedin]
assms[unfolded continuous_map_closedin] by blast

brings it down to practically zero.

This is not very interesting in itself but it raises for me following
questions:

I think this is indeed interesting, and shows that while low level
massaging is frowned upon but it is actually useful, it reduces the
search space much. I would love to see a write up on this. Is there
one?

view this post on Zulip Email Gateway (Aug 13 2025 at 07:35):

From: Tobias Nipkow <nipkow@in.tum.de>
I tuned another slow proof in HOL-Analysis.
Using the timimg panel, I was surprised that this showed up:

Does that have anything to do with the cite command in that text block?

Tobias

On 12/08/2025 21:28, Stepan Holub (via cl-isabelle-users Mailing List) wrote:

Hello,

today I happened to compile "HOL-Analysis.Abstract_Topological_Spaces" which
takes about 5 minutes on my notebook.
Out of curiosity, I looked at the longest "by metis" which takes about
20 s. It is

by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin
continuous_map_closedin)

on line 3310.

A trivial transformation (guessed easily without understanding what is going
on in the proof) to

using closed_real_atLeastAtMost[unfolded closed_closedin]
assms[unfolded continuous_map_closedin]  by blast

brings it down to practically zero.

This is not very interesting in itself but it raises for me following questions:

Stepan

smime.p7s

view this post on Zulip Email Gateway (Aug 13 2025 at 08:34):

From: Manuel Eberl <manuel@pruvisto.org>
Hello,

as a big user of HOL-Analysis: yes, getting rid of a metis call that
runs for this long is definitely a valuable improvement. This timing
information has to be taken with a grain of salt, but 20s seems
excessive even for an outlier.

As Martin pointed out, performance is not the only concern, but as far
as readability and maintainability are concerned, metis calls are
already pretty bad in my opinion, so anything you replace them with is
unlikely to be worse in those regards.

@Martin: You mention "metis_instantiate". What is that? I couldn't find
anything about it.

Manuel

view this post on Zulip Email Gateway (Aug 13 2025 at 08:46):

From: Martin Desharnais <martin.desharnais@posteo.de>
Hi Manuel,

On 13.08.25 10:32, Manuel Eberl wrote:

@Martin: You mention "metis_instantiate". What is that? I couldn't find
anything about it.

Fact instantiation is a new feature in Isabelle2025 implemented by Lukas
Bartl both in Metis and Sledgehammer. It is described in the
Sledgehammer documentation.

The metis option is documented in § 6.2:

The metis method also supports the Isabelle option
[[metis_instantiate]], which tells metis to infer and suggest
instantiations of facts using of from a successful proof.

The Sledgehammer option is documented in § 7.4:

instantiate [= smart_bool]
Specifies whether Metis should try to infer variable instantiations
be fore proof reconstruction, which results in instantiations of facts
using of (e.g. map_prod_surj_on[of f A "f A" g B "g B"]). This can
make the proof methods faster and more intelligible. If the option is
set to smart (the default), variable instantiations are inferred only
if proof reconstruction failed or timed out. (

See the following CADE-30 paper for details:

Lukas Bartl, Jasmin Blanchette and Tobias Nipkow. Exploiting
Instantiations from Paramodulation Proofs in Isabelle/HOL.

Regards,
Martin

view this post on Zulip Email Gateway (Aug 13 2025 at 08:47):

From: Tobias Nipkow <nipkow@in.tum.de>
metis_instantiate:
https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette/inst.pdf

It is the new secret weapon to simplify metis proofs. Once you have a metis
proof, you precede it with "using [[metis_instantiate]]" and it spits out a
metis proof where the facts are instantiated (with "of") as much as possible.
That proof tends to run more quickly, but you can also try to turn it into a
simp/auto/etc proof by trying something like

using <key instantiated facts> by simp/auto/etc

and leaving out all the trivial lemmas that cluter up the metis proof.

Sometimes it helps...

Tobias

On 13/08/2025 10:32, Manuel Eberl wrote:

@Martin: You mention "metis_instantiate". What is that? I couldn't find anything
about it.

smime.p7s

view this post on Zulip Email Gateway (Aug 13 2025 at 09:32):

From: Manuel Eberl <manuel@pruvisto.org>
Okay, that's exactly what I thought it would be and it's amazing. Well,
I assume it is, I haven't tried it yet. But I've been wanting something
like this for a long time.

Thanks to you all!

Manuel

On 13/08/2025 10:47, Tobias Nipkow wrote:

metis_instantiate:
https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette/inst.pdf

It is the new secret weapon to simplify metis proofs. Once you have a
metis proof, you precede it with "using [[metis_instantiate]]" and it
spits out a metis proof where the facts are instantiated (with "of")
as much as possible. That proof tends to run more quickly, but you can
also try to turn it into a simp/auto/etc proof by trying something like

using <key instantiated facts> by simp/auto/etc

and leaving out all the trivial lemmas that cluter up the metis proof.

Sometimes it helps...

Tobias

On 13/08/2025 10:32, Manuel Eberl wrote:

@Martin: You mention "metis_instantiate". What is that? I couldn't
find anything about it.

view this post on Zulip Email Gateway (Aug 13 2025 at 09:43):

From: Fabian Huch <huch@in.tum.de>

On 8/13/25 09:19, Martin Desharnais wrote:

Hi Stepan,

On 12.08.25 21:28, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:

Out of curiosity, I looked at the longest "by metis" which takes about
20 s. It is

by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin
continuous_map_closedin)

on line 3310.

A trivial transformation (guessed easily without understanding what
is going on in the proof) to

using closed_real_atLeastAtMost[unfolded closed_closedin]
assms[unfolded continuous_map_closedin]  by blast

brings it down to practically zero.

I checked the mentioned theory and found two duplicates of the proof
you presented, each of which taking approximately 7.5 seconds on my
laptop. I (very slightly) generalized the proof step, proved it with
your suggested proof, and reused the generalized proof step in both
places (See Isabelle/7ac70210d12c).

This is not very interesting in itself but it raises for me following
questions:

I suspect that many the verification of many formalizations could be
sped up by tuning some of the proofs.

As for caring about it, opinions may vary. I believe that one should
strive for a balance between readability, maintainability, and
verification performance; verification performance not only reduce the
running time, but also the energy consumption.

I believe the change you proposed was a good one, because it improved
both readability and performance.

Yes, some proof refactoring could be automated if one was to invest
the time into writing a tool.

I wrote a tool for this once, but wasn't fully satisfied by the
approach: It uses a build hook, which makes it very difficult to obtain
local facts used in a proof. A better (but even less scalable) approach
would be to use an interactive session for this. The second problem was
an issue with threading, where after starting a large number of threads
(to process many goals) the system became unresponsive.

To obtain a good ranking for proofs, one also needs to obtain data on
which proofs are preferred. I attempted to get responses for this once
(from the AFP editors) but didn't receive too many.

If someone wants to pick this up, I am happy to share the prototype.

Fabian

Last updated: Aug 20 2025 at 20:23 UTC