simp? often unnecessarily reports eq_self_iff_true

Stream: general

[Scott Morrison]

simp? very often includes eq_self_iff_true in its suggestion list, and I find that in almost every case this is not needed. Can we do something about this?

[Johan Commelin]

In some sense simp? is a pretty experimental feature. I hacked it together without being an expert on simp or C++. I'm grateful for the help that I received from experts. But I take all the blame for the hiccups. And unfortunately I don't think I'm qualified to make it better :sad:

[Scott Morrison]

I just experimented a bit, and I can't actually find a single spurious appearance of eq_self_iff_true in uses of simp only [...] in mathlib.

[Scott Morrison]

So I think I was just getting unlucky, and it's not a pervasive problem.

[Johan Commelin]

Still, it's a bug. I must have implemented some of the tracing incorrectly