simp normal form for `Iio ⊤`

Stream: general

[Yury G. Kudryashov]

/poll What should be the simp normal forms for Iio ⊤ and Ico a ⊤?
Iio ⊤ and Ico a ⊤
{⊤}ᶜ and Ico a ⊤
Iio ⊤ and Ici a \ {⊤}
{⊤}ᶜ and Ici a \ {⊤}

[Yury G. Kudryashov]

Note that we simplify Ici ⊤ to {⊤}.

[Yury G. Kudryashov]

Motivated by @Eric Wieser 's comment in #14296.

[Yaël Dillies]

It's 0 < n vs n ≠ 0 all over again. So we would like to simplify towards a < ⊤ in hypotheses and towards a ≠ ⊤` in the goal. But of course simp can't detect that.

[Yury G. Kudryashov]

I'll merge the PR now, then change it if needed in the PR that will add the simp lemmas.

[Yury G. Kudryashov]

For now, the answer is "nobody cares".

[Reid Barton]

I don't really care but if I had to choose, I would probably choose the first option

[Reid Barton]

Singletons are a bit different I feel, we know those are also intervals just by looking at them.

[Yaël Dillies]

Yeah my guts make me want to stay in the intervals world because a lot of lemmas about their interaction.