coercion and too simp

Stream: general

[Sean Leather]

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]

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]

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]

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

[Sean Leather]

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]

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

[Sean Leather]

Not the rule I expected.

[Sean Leather]

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⟩