rfl lemmas

Stream: general

[Kenny Lau]

how important are rfl-simp-lemmas being rfl?

[Chris Hughes]

I don't understand the question. You mean how important is it that they're proved using rfl, or that they can be proved using rfl or something completely different?

[Kenny Lau]

should we depend on rfl lemmas being rfl (so that we can use dsimp instead of simp)?

[Scott Morrison]

Yes, it's important... I think the point is that dsimp just changes the goal, while simp has to actually construct the proof, and sometimes that goes wrong. I should be able to be more specific (as someone explaining to me this difference actually made a big difference in the behaviour of tidy), but I'm having trouble thinking of an example now.