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



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.



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