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: Dec 20 2023 at 11:08 UTC