simp and unfolding

Stream: new members

[Alistair Tucker]

I thought it might work to have these simp lemmas:

@[simp] lemma with_bot.coe_sup {α : Type*} [semilattice_sup α] (a b : α) :
  ((a ⊔ b : α) : with_bot α) = (a : with_bot α) ⊔ (b : with_bot α) := rfl

@[simp] lemma with_top.coe_sup {α : Type*} [semilattice_sup α] (a b : α) :
  ((a ⊔ b : α) : with_top α) = (a : with_top α) ⊔ (b : with_top α) := rfl

But it seems like simp will only ever use one (the more recently defined) for both cases, which would make it a pretty bad idea. I guess it sees the left hand side of both as just ((a ⊔ b : α) : option α)?

[Alistair Tucker]

Was just wondering if there was some way to make this work

[Eric Wieser]

I'm pretty sure I saw this in a recent PR. An easy compromise is to remove @[simp] from one of them, and add comments that reference each other.

[Mario Carneiro]

No, adding @[simp] to just one would be bad because the ⊔ on the right is annotated with the with_bot type so if it fires on a with_top goal then you will get type confusion issues

[Kevin Buzzard]

This is exactly why we should just have three isomorphic types and duplicate a load of code :-)

[Eric Wieser]

irreducible would fix this, right?

[Mario Carneiro]

I think they are already irreducible. This is a bug in simp which has already caused problems for mathport

[Alistair Tucker]

Thanks! That may have been my PR #6922. I have removed the @[simp] tags for the moment.
I don't know about irreducible but a quick search for the term in bounded_lattice.lean does not yield any results.

[Sebastien Gouezel]

I don't think they're irreducible. This has been discussed several times, but I don't think it made it to mathlib.