Stream: new members

Topic: simp and unfolding

Alistair Tucker (Mar 28 2021 at 10:16):

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 (Mar 28 2021 at 10:17):

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

Eric Wieser (Mar 28 2021 at 10:58):

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 (Mar 28 2021 at 11:01):

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 (Mar 28 2021 at 11:37):

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

Eric Wieser (Mar 28 2021 at 12:22):

irreducible would fix this, right?

Mario Carneiro (Mar 28 2021 at 12:41):

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

Alistair Tucker (Mar 28 2021 at 12:54):

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 (Mar 28 2021 at 13:19):

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

Last updated: May 10 2021 at 00:31 UTC