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



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

On 03/07/2021 23:32, Lawrence Paulson wrote:
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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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