Email Gateway (Aug 22 2022 at 19:51): 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: Nov 21 2024 at 12:39 UTC