# Zulip Chat Archive

## 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`
```

(docs#canonically_linear_ordered_add_monoid)

#### 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.

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

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

#### 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