[isabelle] s/h: bogus proofs from e



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





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