# Re: [isabelle] A bug in chained proof mode

One possible explanation of your issue could be that the symbol f has a polymorphic type, so that the two instances don’t match. So it would be better if you could submit a self-contained theory.
Larry Paulson
On 11 Jun 2014, at 06:03, Eddy Westbrook <westbrook at kestrel.edu> wrote:
> Hi,
>
> I think I have found a bug in the chained proof mode, that occurs for equality proofs if one of the proof used in the chain is a reflexive proof. As an example, the following proof fails, even though (as far as I understand the chain mode) it should succeed:
>
> lemma chain_bug: "e1 = e2 ⟹ f e1 = f e2"
> proof -
> assume eq1: "e1 = e2"
> have "f e1 = f e2" by (rule arg_cong[OF eq1])
> also
> have "f e2 = f e2" by (simp)
> finally
> have "f e1 = f e2".
> qed
>
> Although it may seem silly to write a proof that “f e2 = f e2”, the reason it comes up is that the proof is machine-generated, and sometimes it is easier to generate a proof that something equals itself rather than checking explicitly for that fact.
>
> Anyway, just thought I would report this.
>
> Thanks,
> -Eddy
>

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