Re: [isabelle] Reflexive rewriting

On Mon, 13 Jul 2015, Manuel Eberl wrote:

I know how to fix this with NO_MATCH, but my question is this: why do we not introduce a check in the simplifier that prevents it from rewriting a term to itself? I don't know much about the simplifier, but I should be surprised if such a check were difficult to implement, and I do not think there would be a significant loss of performance. It also should not break any existing proofs or code.

I am also not an expert on the Simplifier myself, but by default the blind assumptions above need to be inverted. Just empirically, any tiny change anywhere will cause lots of unexpected problems in obscure places.

This does not mean, reforms should not be done -- we do it all the time. But it usually takes really long and hard work to push a change through.


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