## Stream: general

### Topic: Simp normal form: bot_eq_zero, zero_eq_bot

#### Eric Wieser (Jun 03 2022 at 23:34):

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 (Jun 03 2022 at 23:36):

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 (Jun 03 2022 at 23:38):

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


#### Yury G. Kudryashov (Jun 04 2022 at 01:35):

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.

#### Kevin Buzzard (Jun 04 2022 at 05:46):

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 (Jun 04 2022 at 05:47):

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

#### Damiano Testa (Jun 04 2022 at 05:47):

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

#### Violeta Hernández (Jun 04 2022 at 06:02):

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 (Jun 04 2022 at 08:47):

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

#### Riccardo Brasca (Jun 04 2022 at 08:51):

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 (Jun 04 2022 at 10:01):

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

#### Eric Wieser (Jun 04 2022 at 10:47):

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 (Jun 04 2022 at 10:50):

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

Last updated: Aug 03 2023 at 10:10 UTC