*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] s/h: bogus proofs from e*From*: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Mon, 12 Jul 2021 16:51:21 +0200*Authentication-results*: cam.ac.uk; iprev=pass (mailin.vu.nl) smtp.remote-ip=130.37.164.82; spf=pass smtp.mailfrom=vu.nl; arc=none*Cc*: Isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <715EE017-92DC-4C41-A9B7-99BAF909B7FD@cam.ac.uk>*References*: <715EE017-92DC-4C41-A9B7-99BAF909B7FD@cam.ac.uk>*Reply-to*: Jasmin Blanchette <j.c.blanchette at vu.nl>

Hi Larry, > 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? 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.

**Follow-Ups**:**Re: [isabelle] s/h: bogus proofs from e***From:*Asta Halkjær From

**References**:**[isabelle] s/h: bogus proofs from e***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Sorting algorithms in the AFP
- Next by Date: Re: [isabelle] s/h: bogus proofs from e
- Previous by Thread: Re: [isabelle] s/h: bogus proofs from e
- Next by Thread: Re: [isabelle] s/h: bogus proofs from e
- Cl-isabelle-users July 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list