Zulip Chat Archive

Stream: general

Topic: coercion and too simp


Sean Leather (Jun 07 2018 at 08:30):

I keep running into the problem of simp reducing something to p = ff when I really want ¬↥p. I then end up doing a rw explicitly, which is a pain. Is there any way to work around this issue with simp?

Kevin Buzzard (Jun 07 2018 at 08:34):

You can often do suffices : <what you want>, simpa using this or ...simp [this] or similar. You want something neater than this though?

Sean Leather (Jun 07 2018 at 08:36):

I was hoping for something like simp [-<theorem>], disabling a particular rewrite but still using only simp. I'm not sure those other options are any better than the rw that I do now.

Sean Leather (Jun 07 2018 at 08:37):

Or, even better, remove the simp attribute locally for my whole file. :simple_smile:

Sean Leather (Jun 07 2018 at 08:44):

Ah, found it: simp [-eq_ff_eq_not_eq_tt]. I just had to look at the simp rules with set_option trace.simplify.rewrite true.

Sean Leather (Jun 07 2018 at 08:44):

@[simp] lemma eq_ff_eq_not_eq_tt (b : bool) : (¬(b = tt)) = (b = ff)

Sean Leather (Jun 07 2018 at 08:45):

Not the rule I expected.

Sean Leather (Jun 07 2018 at 08:46):

But I guess it makes sense due to this instance and defeq:

@[reducible] instance coe_sort_bool : has_coe_to_sort bool := Prop, λ y, y = tt

Last updated: Dec 20 2023 at 11:08 UTC