[isabelle] A bug in chained proof mode



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.