Zulip Chat Archive

Stream: general

Topic: rfl lemmas


view this post on Zulip Kenny Lau (Sep 05 2018 at 18:50):

how important are rfl-simp-lemmas being rfl?

view this post on Zulip Chris Hughes (Sep 05 2018 at 19:05):

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?

view this post on Zulip Kenny Lau (Sep 05 2018 at 19:07):

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

view this post on Zulip Scott Morrison (Sep 06 2018 at 04:35):

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.


Last updated: May 15 2021 at 22:14 UTC