*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Isabelle2019-RC2: Sledgehammer and the name of variables*From*: José Manuel Rodríguez Caballero <josephcmac at gmail.com>*Date*: Thu, 16 May 2019 02:46:56 +0300

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.

- Previous by Date: [isabelle] Isabelle2019-RC2: Prover errors when using sledgehammer
- Next by Date: Re: [isabelle] Isabelle2019-RC2: Prover errors when using sledgehammer
- Previous by Thread: Re: [isabelle] Isabelle2019-RC2: Prover errors when using sledgehammer
- Next by Thread: [isabelle] Code generation with type classes leads to compile error
- Cl-isabelle-users May 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list