Email Gateway (Jan 16 2023 at 12:32): Email Gateway (Jan 16 2023 at 12:32):From: David Fuenmayor <davfuenmayor@gmail.com>
Dear Isabelle users and experts:
This is an instance of a recurrent problem I have been having, under
different guises, with (1) Sledgehammer's suggested reconstructions not
working (mostly involving metis), and (2) metis apparent irregular
behaviour (at least to the non-initiated).
As shown in the attached file (whose content I copy-paste below as well),
not only is the metis command, as suggested by sledgehammer, unsuccessful
(without further massaging in the form of definitions' unfolding), but also
is metis behaviour per se irregular (e.g. changes when switching universal
with existential quantifiers as in the example).
Do you have the same problem? or am I doing something wrong?
(Fyi, I am using Isabelle 2022 on linux.)
Thanks for your help!
David
theory example
imports Main
begin
definition "swap f ≡ λa b. f b a"
definition "Ex2 r ≡ ∃a b. r a b"
definition "All2 r ≡ ∀a b. r a b"
(**Case 1: Using Ex2 definition)
(*The metis reconstruction suggested by sledgehammer does not work out of
the box*)
lemma "Ex2 r = Ex2(swap r)" sledgehammer (* by (metis Ex2_def swap_def) *)
oops (* fails! *)
(Some 'massaging' in the form of definition unfolding is required)
lemma "Ex2 r = Ex2(swap r)" (* using Ex2_def swap_def by metis ) oops (
fails too! *)
lemma "Ex2 r = Ex2(swap r)" unfolding swap_def (* by (metis Ex2_def)*) oops
(* fails too! *)
lemma "Ex2 r = Ex2(swap r)" unfolding Ex2_def by (metis swap_def) (*
succeeds *)
lemma "Ex2 r = Ex2(swap r)" unfolding Ex2_def using swap_def by metis (*
succeeds *)
(**Case 2: Using All2 definition (no problem) ****)
(*By contrast, here the metis reconstruction suggested by sledgehammer
works well out of the box*)
lemma "All2 r = All2(swap r)" sledgehammer by (metis All2_def swap_def) (*
succeeds *)
(and all other variants work too)
lemma "All2 r = All2(swap r)" using All2_def swap_def by metis (* succeeds
*)
lemma "All2 r = All2(swap r)" unfolding All2_def swap_def by metis (*
succeeds *)
(**Questions:
end
example.thy
Email Gateway (Jan 19 2023 at 16:35):From: David Fuenmayor <davfuenmayor@gmail.com>
I would like to recall this message (which apparently got lost among the
latest ranting against rank1 polymorphism).
As a grateful user of sledgehammer, I have come to believe that this sort
of tools really are the key to widespread (and game-changing!) adoption of
proof assistants in the mathematical world (more so than eg.
overcomplicating the type system).
So please interpret my previous message as a constructive bug(?)
reporting. I am open to suggestions on how to be a better user of this tool
(or even contribute to it?).
Email Gateway (Feb 13 2023 at 12:04):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear David,
First, I'm sorry for the big delay in answering your email. Part of the reason is that your email originally landed in my spam folder! Be assured that feedback about Sledgehammer's misbehaviors is always welcome.
Now let's look at your theory:
(The metis reconstruction suggested by sledgehammer does not work out of the box)
lemma "Ex2 r = Ex2(swap r)" sledgehammer (* by (metis Ex2_def swap_def) ) oops ( fails! *)
This is visible from the fact that no time indication is printed next to the metis call (e.g. "(0.4 s)"). In the repository version of Isabelle (and hence, likely, in the next official version), this will be more explicitly labeled as "(> 1.0 s, timed out)".
To answer your questions:
- Why does sledgehammer suggested reconstruction fail in case 1?
Because it fails. Or rather, it seems to take too much time. Reconstruction is not a perfect art, and because different encodings can be used by Sledgehammer and metis, there's no guarantee that a Sledgehammer/ATP proof will be reconstructible by metis. This is why Sledgehammer tests the metis calls (and other proof methods like "auto" and "simp") and suggests something that works if it can and that times out if it finds nothing.
The lack of specific information in Isabelle2022 is unfortunate, and was also involuntary (older versions of Isabelle said "(> 1.0 s, timed out)").
- Why does metis work differently in cases 1 and 2?
Because it's a different proof goal. Metis is a highly heuristic prover and any change in the goal can lead it to perform wildly differently.
Regards,
Jasmin
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of David Fuenmayor <davfuenmayor@gmail.com>
Sent: Thursday, January 19, 2023 17:35
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] Sledgehammer reconstructions fail (+ irregular behaviour of metis)
I would like to recall this message (which apparently got lost among the latest ranting against rank1 polymorphism).
As a grateful user of sledgehammer, I have come to believe that this sort of tools really are the key to widespread (and game-changing!) adoption of proof assistants in the mathematical world (more so than eg. overcomplicating the type system).
So please interpret my previous message as a constructive bug(?) reporting. I am open to suggestions on how to be a better user of this tool (or even contribute to it?).
On Mon, 16 Jan 2023, 13:32 David Fuenmayor <davfuenmayor@gmail.com<mailto:davfuenmayor@gmail.com>> wrote:
Dear Isabelle users and experts:
This is an instance of a recurrent problem I have been having, under different guises, with (1) Sledgehammer's suggested reconstructions not working (mostly involving metis), and (2) metis apparent irregular behaviour (at least to the non-initiated).
As shown in the attached file (whose content I copy-paste below as well), not only is the metis command, as suggested by sledgehammer, unsuccessful (without further massaging in the form of definitions' unfolding), but also is metis behaviour per se irregular (e.g. changes when switching universal with existential quantifiers as in the example).
Do you have the same problem? or am I doing something wrong?
(Fyi, I am using Isabelle 2022 on linux.)
Thanks for your help!
David
theory example
imports Main
begin
definition "swap f ≡ λa b. f b a"
definition "Ex2 r ≡ ∃a b. r a b"
definition "All2 r ≡ ∀a b. r a b"
(**Case 1: Using Ex2 definition)
(The metis reconstruction suggested by sledgehammer does not work out of the box)
lemma "Ex2 r = Ex2(swap r)" sledgehammer (* by (metis Ex2_def swap_def) ) oops ( fails! *)
(Some 'massaging' in the form of definition unfolding is required)
lemma "Ex2 r = Ex2(swap r)" (* using Ex2_def swap_def by metis ) oops ( fails too! *)
lemma "Ex2 r = Ex2(swap r)" unfolding swap_def (* by (metis Ex2_def)) oops ( fails too! *)
lemma "Ex2 r = Ex2(swap r)" unfolding Ex2_def by (metis swap_def) (* succeeds *)
lemma "Ex2 r = Ex2(swap r)" unfolding Ex2_def using swap_def by metis (* succeeds *)
(**Case 2: Using All2 definition (no problem) ****)
(By contrast, here the metis reconstruction suggested by sledgehammer works well out of the box)
lemma "All2 r = All2(swap r)" sledgehammer by (metis All2_def swap_def) (* succeeds *)
(and all other variants work too)
lemma "All2 r = All2(swap r)" using All2_def swap_def by metis (* succeeds *)
lemma "All2 r = All2(swap r)" unfolding All2_def swap_def by metis (* succeeds *)
(**Questions:
end
Email Gateway (Feb 13 2023 at 18:42):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear David,
I have looked more closely into the metis failure and found out that it was due to a misbehavior of the preprocessor (the clausifier). This is some really old code that failed when faced with nested lambdas where some inner lambda can be eta-reduced (as in "%x y. r x y"). I have now found a solution that doesn't break any proof in Isabelle or the AFP and that makes your example work. The patch is now part of the development version and will likely be part of the next release. Thanks again for your report.
Best,
Jasmin
From: Blanchette, J.C. (Jasmin Christian) <j.c.blanchette@vu.nl>
Sent: Monday, February 13, 2023 13:03
To: David Fuenmayor <davfuenmayor@gmail.com>; cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] Sledgehammer reconstructions fail (+ irregular behaviour of metis)
Dear David,
First, I'm sorry for the big delay in answering your email. Part of the reason is that your email originally landed in my spam folder! Be assured that feedback about Sledgehammer's misbehaviors is always welcome.
Now let's look at your theory:
(The metis reconstruction suggested by sledgehammer does not work out of the box)
lemma "Ex2 r = Ex2(swap r)" sledgehammer (* by (metis Ex2_def swap_def) ) oops ( fails! *)
This is visible from the fact that no time indication is printed next to the metis call (e.g. "(0.4 s)"). In the repository version of Isabelle (and hence, likely, in the next official version), this will be more explicitly labeled as "(> 1.0 s, timed out)".
To answer your questions:
- Why does sledgehammer suggested reconstruction fail in case 1?
Because it fails. Or rather, it seems to take too much time. Reconstruction is not a perfect art, and because different encodings can be used by Sledgehammer and metis, there's no guarantee that a Sledgehammer/ATP proof will be reconstructible by metis. This is why Sledgehammer tests the metis calls (and other proof methods like "auto" and "simp") and suggests something that works if it can and that times out if it finds nothing.
The lack of specific information in Isabelle2022 is unfortunate, and was also involuntary (older versions of Isabelle said "(> 1.0 s, timed out)").
- Why does metis work differently in cases 1 and 2?
Because it's a different proof goal. Metis is a highly heuristic prover and any change in the goal can lead it to perform wildly differently.
Regards,
Jasmin
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of David Fuenmayor <davfuenmayor@gmail.com>
Sent: Thursday, January 19, 2023 17:35
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] Sledgehammer reconstructions fail (+ irregular behaviour of metis)
I would like to recall this message (which apparently got lost among the latest ranting against rank1 polymorphism).
As a grateful user of sledgehammer, I have come to believe that this sort of tools really are the key to widespread (and game-changing!) adoption of proof assistants in the mathematical world (more so than eg. overcomplicating the type system).
So please interpret my previous message as a constructive bug(?) reporting. I am open to suggestions on how to be a better user of this tool (or even contribute to it?).
On Mon, 16 Jan 2023, 13:32 David Fuenmayor <davfuenmayor@gmail.com<mailto:davfuenmayor@gmail.com>> wrote:
Dear Isabelle users and experts:
This is an instance of a recurrent problem I have been having, under different guises, with (1) Sledgehammer's suggested reconstructions not working (mostly involving metis), and (2) metis apparent irregular behaviour (at least to the non-initiated).
As shown in the attached file (whose content I copy-paste below as well), not only is the metis command, as suggested by sledgehammer, unsuccessful (without further massaging in the form of definitions' unfolding), but also is metis behaviour per se irregular (e.g. changes when switching universal with existential quantifiers as in the example).
Do you have the same problem? or am I doing something wrong?
(Fyi, I am using Isabelle 2022 on linux.)
Thanks for your help!
David
theory example
imports Main
begin
definition "swap f ≡ λa b. f b a"
definition "Ex2 r ≡ ∃a b. r a b"
definition "All2 r ≡ ∀a b. r a b"
(**Case 1: Using Ex2 definition)
(The metis reconstruction suggested by sledgehammer does not work out of the box)
lemma "Ex2 r = Ex2(swap r)" sledgehammer (* by (metis Ex2_def swap_def) ) oops ( fails! *)
(Some 'massaging' in the form of definition unfolding is required)
lemma "Ex2 r = Ex2(swap r)" (* using Ex2_def swap_def by metis ) oops ( fails too! *)
lemma "Ex2 r = Ex2(swap r)" unfolding swap_def (* by (metis Ex2_def)) oops ( fails too! *)
lemma "Ex2 r = Ex2(swap r)" unfolding Ex2_def by (metis swap_def) (* succeeds *)
lemma "Ex2 r = Ex2(swap r)" unfolding Ex2_def using swap_def by metis (* succeeds *)
(**Case 2: Using All2 definition (no problem) ****)
(By contrast, here the metis reconstruction suggested by sledgehammer works well out of the box)
lemma "All2 r = All2(swap r)" sledgehammer by (metis All2_def swap_def) (* succeeds *)
(and all other variants work too)
lemma "All2 r = All2(swap r)" using All2_def swap_def by metis (* succeeds *)
lemma "All2 r = All2(swap r)" unfolding All2_def swap_def by metis (* succeeds *)
(**Questions:
end
Email Gateway (Feb 13 2023 at 20:27):From: David Fuenmayor <davfuenmayor@gmail.com>
Dear Jasmin
That was really quick. Thank you!
I take the opportunity to ask you about a possibly (un)related issue:
I have noticed that 'massaging' the goals by manually unfolding definitions
tends to significantly improve both sledgehammer's performance (external
ATPs now finding proofs) and metis reconstructions (which otherwise fail
when the relevant XX_def(s) are only provided as an argument). In many
cases unfolding the first 'layer' of definitions already works wonders. So
I was wondering whether some sort of 'heuristic definitions unfolding'
could be part of sledgehammer's repertoire? Does this make sense from your
perspective?
Best
David
Email Gateway (Feb 14 2023 at 13:01):From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear David,
The idea makes sense, but it's a bit of a can of worms: What and how far should we unfold? Maybe it's something that should be implemented in a higher-order prover like Zipperposition instead of a preprocessor, although admittedly for reconstruction to work optimally we should then unfold the same definitions as during proof search. I'm taking a note.
Best,
Jasmin
From: David Fuenmayor <davfuenmayor@gmail.com>
Sent: Monday, February 13, 2023 21:26
To: Blanchette, J.C. (Jasmin Christian) <j.c.blanchette@vu.nl>
Cc: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] Sledgehammer reconstructions fail (+ irregular behaviour of metis)
Dear Jasmin
That was really quick. Thank you!
I take the opportunity to ask you about a possibly (un)related issue:
I have noticed that 'massaging' the goals by manually unfolding definitions tends to significantly improve both sledgehammer's performance (external ATPs now finding proofs) and metis reconstructions (which otherwise fail when the relevant XX_def(s) are only provided as an argument). In many cases unfolding the first 'layer' of definitions already works wonders. So I was wondering whether some sort of 'heuristic definitions unfolding' could be part of sledgehammer's repertoire? Does this make sense from your perspective?
Best
David
On Mon, Feb 13, 2023 at 7:42 PM Blanchette, J.C. (Jasmin Christian) <j.c.blanchette@vu.nl<mailto:j.c.blanchette@vu.nl>> wrote:
Dear David,
I have looked more closely into the metis failure and found out that it was due to a misbehavior of the preprocessor (the clausifier). This is some really old code that failed when faced with nested lambdas where some inner lambda can be eta-reduced (as in "%x y. r x y"). I have now found a solution that doesn't break any proof in Isabelle or the AFP and that makes your example work. The patch is now part of the development version and will likely be part of the next release. Thanks again for your report.
Best,
Jasmin
From: Blanchette, J.C. (Jasmin Christian) <j.c.blanchette@vu.nl<mailto:j.c.blanchette@vu.nl>>
Sent: Monday, February 13, 2023 13:03
To: David Fuenmayor <davfuenmayor@gmail.com<mailto:davfuenmayor@gmail.com>>; cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk> <cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>>
Subject: Re: [isabelle] Sledgehammer reconstructions fail (+ irregular behaviour of metis)
Dear David,
First, I'm sorry for the big delay in answering your email. Part of the reason is that your email originally landed in my spam folder! Be assured that feedback about Sledgehammer's misbehaviors is always welcome.
Now let's look at your theory:
(The metis reconstruction suggested by sledgehammer does not work out of the box)
lemma "Ex2 r = Ex2(swap r)" sledgehammer (* by (metis Ex2_def swap_def) ) oops ( fails! *)
This is visible from the fact that no time indication is printed next to the metis call (e.g. "(0.4 s)"). In the repository version of Isabelle (and hence, likely, in the next official version), this will be more explicitly labeled as "(> 1.0 s, timed out)".
To answer your questions:
- Why does sledgehammer suggested reconstruction fail in case 1?
Because it fails. Or rather, it seems to take too much time. Reconstruction is not a perfect art, and because different encodings can be used by Sledgehammer and metis, there's no guarantee that a Sledgehammer/ATP proof will be reconstructible by metis. This is why Sledgehammer tests the metis calls (and other proof methods like "auto" and "simp") and suggests something that works if it can and that times out if it finds nothing.
The lack of specific information in Isabelle2022 is unfortunate, and was also involuntary (older versions of Isabelle said "(> 1.0 s, timed out)").
- Why does metis work differently in cases 1 and 2?
Because it's a different proof goal. Metis is a highly heuristic prover and any change in the goal can lead it to perform wildly differently.
Regards,
Jasmin
From: cl-isabelle-users-request@lists.cam.ac.uk<mailto:cl-isabelle-users-request@lists.cam.ac.uk> <cl-isabelle-users-request@lists.cam.ac.uk<mailto:cl-isabelle-users-request@lists.cam.ac.uk>> on behalf of David Fuenmayor <davfuenmayor@gmail.com<mailto:davfuenmayor@gmail.com>>
Sent: Thursday, January 19, 2023 17:35
To: cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk> <cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>>
Subject: Re: [isabelle] Sledgehammer reconstructions fail (+ irregular behaviour of metis)
I would like to recall this message (which apparently got lost among the latest ranting against rank1 polymorphism).
As a grateful user of sledgehammer, I have come to believe that this sort of tools really are the key to widespread (and game-changing!) adoption of proof assistants in the mathematical world (more so than eg. overcomplicating the type system).
So please interpret my previous message as a constructive bug(?) reporting. I am open to suggestions on how to be a better user of this tool (or even contribute to it?).
On Mon, 16 Jan 2023, 13:32 David Fuenmayor <davfuenmayor@gmail.com<mailto:davfuenmayor@gmail.com>> wrote:
Dear Isabelle users and experts:
This is an instance of a recurrent problem I have been having, under different guises, with (1) Sledgehammer's suggested reconstructions not working (mostly involving metis), and (2) metis apparent irregular behaviour (at least to the non-initiated).
As shown in the attached file (whose content I copy-paste below as well), not only is the metis command, as suggested by sledgehammer, unsuccessful (without further massaging in the form of definitions' unfolding), but also is metis behaviour per se irregular (e.g. changes when switching universal with existential quantifiers as in the example).
Do you have the same problem? or am I doing something wrong?
(Fyi, I am using Isabelle 2022 on linux.)
Thanks for your help!
David
theory example
imports Main
begin
definition "swap f ≡ λa b. f b a"
definition "Ex2 r ≡ ∃a b. r a b"
definition "All2 r ≡ ∀a b. r a b"
(**Case 1: Using Ex2 definition)
(The metis reconstruction suggested by sledgehammer does not work out of the box)
lemma "Ex2 r = Ex2(swap r)" sledgehammer (* by (metis Ex2_def swap_def) ) oops ( fails! *)
(Some 'massaging' in the form of definition unfolding is required)
lemma "Ex2 r = Ex2(swap r)" (* using Ex2_def swap_def by metis ) oops ( fails too! *)
lemma "Ex2 r = Ex2(swap r)" unfolding swap_def (* by (metis Ex2_def)) oops ( fails too! *)
lemma "Ex2 r = Ex2(swap r)" unfolding Ex2_def by (metis swap_def) (* succeeds *)
lemma "Ex2 r = Ex2(swap r)" unfolding Ex2_def using swap_def by metis (* succeeds *)
(**Case 2: Using All2 definition (no problem) ****)
(By contrast, here the metis reconstruction suggested by sledgehammer works well out of the box)
lemma "All2 r = All2(swap r)" sledgehammer by (metis All2_def swap_def) (* succeeds *)
(and all other variants work too)
lemma "All2 r = All2(swap r)" using All2_def swap_def by metis (* succeeds *)
lemma "All2 r = All2(swap r)" unfolding All2_def swap_def by metis (* succeeds *)
(**Questions:
end
Last updated: Apr 18 2024 at 16:19 UTC