Email Gateway (Jul 03 2021 at 21:32): Email Gateway (Jul 03 2021 at 21:32):From: Lawrence Paulson <lp15@cam.ac.uk>
I’ve been getting a lot of junk sledgehammer proofs from e lately. Finally I found a reproducible example that can be run from a standard theory setup: simply HOL-Analysis. Then try it on
lemma vector_derivative_of_real_left:
assumes "f differentiable at x"
shows "vector_derivative (λx. of_real (f x)) (at x) = of_real (deriv f x)"
by (metis UNIV_I add_diff_cancel_left' assms cancel_comm_monoid_add_class.diff_cancel diff_add_cancel diff_zero differentiable_at_withinI differentiable_compose differentiable_const has_vector_derivative_const has_vector_derivative_transform of_real_differentiable of_real_eq_0_iff of_real_eq_1_iff vector_derivative_const_at vector_derivative_unique_at vector_derivative_works)
Generally these proofs involve theorems like add_diff_cancel_left’ and diff_add_cancel. They are only found by e and they never work. Some output formatting issue?
Larry
Email Gateway (Jul 04 2021 at 14:09):From: Tobias Nipkow <nipkow@in.tum.de>
I have noticed a similar problem recently, but associated more with meson and
verit. Unfortnately I cannot provide a conctrete example right now and cannot
say if add_diff_cancel_left' has anything to do with it, but arithmetic is
certainly involved.
Tobias
smime.p7s
Email Gateway (Jul 04 2021 at 16:28):From: Lawrence Paulson <lp15@cam.ac.uk>
A problem I’ve often noticed is that meson proofs fail, but replacing “meson” by “metis” creates a working proof.
Larry
Email Gateway (Jul 12 2021 at 14:51):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Larry,
I've looked into this one and it turns out E can refind its own proof if given enough time. That's a sign that the issue is either E unsoundness (unlikely) or simply weakness of reconstruction (more likely). This proof in particular relies on the very explosive axiom "X = fTrue \/ X = fFalse" (where X : bool), which Metis, like any reasonable superposition prover, probably weighs down in its clause selection heuristic because X matches anything. (This is the evil case that goes by the name "paramodulation from variable".)
Assuming my analysis is correct, it's unfortunate that you get so many unreconstructable in that area. Perhaps try setting [no_atp] on some offending lemma?
If you have any indication that no proof should be possible from the above lemmas or other sets of lemmas, let me know.
TODO for myself: Repair/improve Isar proof reconstruction so that it provides some useful output in such cases, even if that output is too ugly for inclusion in a user's theory.
Cheers,
Jasmin
P.S. Concerning meson failures, which you mentioned in a followup email: I'm a taker for any reproducible failure.
Email Gateway (Jul 12 2021 at 15:05):From: Asta Halkjær From <andro.from@gmail.com>
I find that meson is very sensitive to "using" lemmas vs feeding them as
arguments and that sledgehammer ignores this.
In my recent AFP entry on Public Announcement Logic I ran into this a lot.
It's unfortunately not a small example, but for instance in the following
lines:
ultimately have ‹⊢⇩! ([r]⇩! K⇩! i p ❙⟷⇩! r ❙⟶⇩! K⇩! i (reduce' r p))›
using Iff_Iff sledgehammer
by (meson Iff_sym Iff_wk)
Sledgehammer provides the meson proof which fails ("Failed to apply initial
proof method") but is easily fixed by either:
The theory:
https://foss.heptapod.net/isa-afp/afp-2021/-/blob/branch/default/thys/Public_Announcement_Logic/PAL.thy#L344
Asta
Den man. 12. jul. 2021 kl. 16.53 skrev Jasmin Blanchette via
Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>:
Email Gateway (Jul 13 2021 at 08:59):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Asta,
I find that meson is very sensitive to "using" lemmas vs feeding them as arguments and that sledgehammer ignores this.
Thank you for your report. Thanks to your example, I was able to track down the issue and find a solution for the Isabelle development version.
Cheers,
Jasmin
Email Gateway (Nov 05 2021 at 09:08):From: Tobias Nipkow <nipkow@in.tum.de>
On 13/07/2021 10:59, Jasmin Blanchette via Cl-isabelle-users wrote:
Hi Asta,
I find that meson is very sensitive to "using" lemmas vs feeding them as arguments and that sledgehammer ignores this.
Thank you for your report. Thanks to your example, I was able to track down the issue and find a solution for the Isabelle development version.
Somewhat belatedly: Why does meson ignore "using"? Shouldn't it take it into
account like metis, simp etc? Does anybody feel responsible for meson?
Tobias
Cheers,
Jasmin
Email Gateway (Nov 05 2021 at 09:30):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Until your comment, I thought that meson wasn't ignoring "using", but that it was just treating it differently somehow. Now I just convinced myself on a small example that you're probably right. I'll look into it.
Jasmin
Email Gateway (Nov 05 2021 at 09:37):From: Tobias Nipkow <nipkow@in.tum.de>
On 05/11/2021 10:30, Jasmin Blanchette via Cl-isabelle-users wrote:
I find that meson is very sensitive to "using" lemmas vs feeding them as arguments and that sledgehammer ignores this.
Thank you for your report. Thanks to your example, I was able to track down the issue and find a solution for the Isabelle development version.Somewhat belatedly: Why does meson ignore "using"? Shouldn't it take it into account like metis, simp etc? Does anybody feel responsible for meson?
Until your comment, I thought that meson wasn't ignoring "using", but that it was just treating it differently somehow. Now I just convinced myself on a small example that you're probably right. I'll look into it.
You are right, I should have written "seems to be ignoring" because I am not
sure myself what exactly is going on. Thanks for taking a look.
Tobias
Jasmin
Email Gateway (Nov 05 2021 at 10:39):From: Lawrence Paulson <lp15@cam.ac.uk>
I wrote the meson tactic in the 1990s, well before Isar even existed. I don't know who wrote the corresponding method.
Larry
Last updated: Jul 15 2022 at 23:21 UTC