Re: [isabelle] s/h: bogus proofs from e



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:
- switching to metis or
- removing the using (important) and adding the Iff_Iff lemma as an argument to meson.

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 at lists.cam.ac.uk>:
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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.