Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2019-RC2: Sledgehammer and the name of...


view this post on Zulip Email Gateway (Aug 22 2022 at 19:51):

From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hello,
I noticed an interesting phenomenon: In order to prove

have ‹Rep_dual ((a + b) *⇩C x) t = Rep_dual (a *⇩C x + b *⇩C x) t›

I applied sledgehammer and I obtained the following (automatically
generated) proof with several errors.

Isar proof (171 ms):
proof -
have f1: "∀d c. Rep_dual (Abs_dual (λa. c *⇩C Rep_dual d (a::'a))) = (λa.
c *⇩C Rep_dual d a)"
by (metis (no_types) Abs_dual_inverse Rep_dual bounded_clinear_compose
bounded_clinear_scaleC_right mem_Collect_eq)
then have "∀c d da. Rep_dual (Abs_dual (λa. Rep_dual da (a::'a) + c *⇩C
Rep_dual d a)) = (λa. Rep_dual da a + c *⇩C Rep_dual d a)"
by (metis (no_types) Abs_dual_inverse Rep_dual bounded_clinear_add
mem_Collect_eq)
then have "Rep_dual (Abs_dual (λa. a *⇩C Rep_dual x a + b *⇩C Rep_dual x
a)) t = a *⇩C Rep_dual x t + b *⇩C Rep_dual x t"
using f1 by (metis (no_types))
then have "Rep_dual (Abs_dual (λa. a *⇩C Rep_dual x a + b *⇩C Rep_dual x
a)) t = (a + b) *⇩C Rep_dual x t"
by (metis (no_types) scaleC_left.add)
then show ?thesis
using f1 by (simp add: plus_dual_def scaleC_dual_def)
qed

The cause of the errors is that a variable generated by sledgehammer had
the same name as a variable that I already used. I corrected this error by
hand, e.g., I substituted the expression

then have "Rep_dual (Abs_dual (λa. a *⇩C Rep_dual x a + b *⇩C Rep_dual x
a)) t = a *⇩C Rep_dual x t + b *⇩C Rep_dual x t"

by the expression

hence "Rep_dual (Abs_dual (λaa. a *⇩C Rep_dual x aa + b *⇩C
Rep_dual x aa)) t = a *⇩C Rep_dual x t + b *⇩C Rep_dual x t"

where I changed the name "a" by "aa" in order to avoid the ambiguity with
respect to the name of the variable "a".

I think that this correction by hand can be done in an automatic way by
Isabelle/HOL. I hope that this observation will contribute to the
improvement of this proof assistant.

Kind Regards,
José M.


Last updated: Mar 28 2024 at 08:18 UTC