Simp normal form: bot_eq_zero, zero_eq_bot

Stream: general

[Eric Wieser]

In #14529, I realized that docs#submodule is a docs#canonically_ordered_add_monoid.

However, if I register the instance, I get a simp loop between docs#bot_eq_zero and docs#submodule.zero_eq_bot.

Which of these do we want as the simp-normal-form? I can't think of any other cases where we've avoided providing algebraic structure just because it messes with simp, so I'd prefer to avoid the solution of just not registering the instance.

[Eric Wieser]

On nat, nnreal, and ennreal bot_eq_zero is obviously the preferred simp-form; but on submodules, it's probably better to remain in lattice-land

[Eric Wieser]

Is this a sensible solution?

/-- `bot_eq_zero` is only a good simp-normal-form in a linear order. -/
@[simp]
theorem bot_eq_zero' {α : Type u} [canonically_linear_ordered_add_monoid α] :
  ⊥ = 0 :=
bot_eq_zero

-- and remove `@[simp]` from `bot_eq_zero`

(docs#canonically_linear_ordered_add_monoid)

[Yury G. Kudryashov]

AFAIR, I saw a suggestion to generalize this lemma to other cases that include ordinals and measures. I'm on a phone, so can't quickly find the relevant thread. Clearly, zero is the preferred form for ordinals and measures too.

[Yury G. Kudryashov]

Here it is: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/bot_eq_zero_class

[Kevin Buzzard]

In regular math land most people have never seen this weird bot notation but would be quite happy with the concept of the zero module

[Damiano Testa]

I agree. I learned about ⊥ and ⊤ in Lean-land.

[Damiano Testa]

I am very comfortable with the zero module, the zero ring, the zero group...

[Violeta Hernández]

I was proposing a bot_eq_zero_class on another thread (which has been linked already). That class would have ⊥ = 0 as a simp lemma, and would also come with a few lemmas for ⊥ rewritten in terms of 0, like zero_le and max_zero_left.

[Reid Barton]

M + N is just the sup right? Which one is preferred?

[Riccardo Brasca]

I totally agree that in math we prefer the 0-module. On the other hand almost everything in mathlib use the language of lattices for substuff. It seems a little strange to have the 0 submodule but the ⊥ subalgebra.

[Yaël Dillies]

What about not making the general lemma simp and deciding the direction using type-specific lemmas?

[Eric Wieser]

Yaël Dillies said:

What about not making the general lemma simp and deciding the direction using type-specific lemmas?

This is basically a more conservative version of what I suggest above, which is to make 0 the normal form only when the order is linear

[Eric Wieser]

Reid Barton said:

M + N is just the sup right? Which one is preferred?

docs#submodule.add_eq_sup suggests the sup is the preferred spelling