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> 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.