## Stream: new members

### Topic: with_bot

#### Damiano Testa (Apr 23 2021 at 13:23):

Dear All,

I am very confused by the lemma below: can anyone help me to prove it?

I cannot even guess if ⊥ + some a is supposed to be 0, none, ⊥. Should I think that ⊥ is "- infinity"? The monoid already has a zero, so I doubt that it is 0...

Thank you very much!

import algebra.ordered_monoid

{a b : α} (bc : (a : with_bot α) ≤ b) :
(⊥ + some a : with_bot α) ≤ ⊥ + some b :=
begin
end


#### Johan Commelin (Apr 23 2021 at 13:26):

The left hand side could also be \bot + \bot, right?

#### Johan Commelin (Apr 23 2021 at 13:26):

So some a could be any term of with_bot

#### Damiano Testa (Apr 23 2021 at 13:27):

Actually, I might have minimised too much the example: I would really like to understand how to work with \bot...

#### Johan Commelin (Apr 23 2021 at 13:27):

Also, you seem to be mixing some and coe : \a -> with_bot \a

#### Damiano Testa (Apr 23 2021 at 13:27):

This is a step in a bigger proof and I thought that coercion would have helped me.

#### Damiano Testa (Apr 23 2021 at 13:28):

I do not really understand whether \bot + \bot could replace the lhs...

#### Johan Commelin (Apr 23 2021 at 13:28):

What is the simp normal form? Either you should have coe everywhere, or some everywhere

#### Damiano Testa (Apr 23 2021 at 13:28):

I have some further assumptions implying monotonicity of addition before I take with_bot, but I cannot get at them...

#### Johan Commelin (Apr 23 2021 at 13:28):

Damiano Testa said:

I do not really understand whether \bot + \bot could replace the lhs...

I meant that it is also valid in that case.

#### Johan Commelin (Apr 23 2021 at 13:28):

So you can generalize the lemma

#### Damiano Testa (Apr 23 2021 at 13:28):

simp constantly fails...

#### Johan Commelin (Apr 23 2021 at 13:29):

There should be a simp lemma with_bot.some_eq_coe.

#### Damiano Testa (Apr 23 2021 at 13:29):

Ah, yes, it is, and in that case, I think that I managed to prove it: I am casing away from with_bot and this is one of the last remaining steps.

#### Damiano Testa (Apr 23 2021 at 13:29):

so applying simp should change something?

#### Johan Commelin (Apr 23 2021 at 13:30):

Unless the lemma doesn't exist )-;

#### Damiano Testa (Apr 23 2021 at 13:30):

Ok, assumption bc changes to a \leq b with simp.

#### Johan Commelin (Apr 23 2021 at 13:30):

What is the definition of \bot + x? Is it \bot or x?

#### Johan Commelin (Apr 23 2021 at 13:30):

I guess it must be \bot, because \bot + 0 = \bot.

#### Damiano Testa (Apr 23 2021 at 13:30):

as far as I can tell, nothing else changes with simp at *.

#### Johan Commelin (Apr 23 2021 at 13:31):

There should be simp-lemmas for this.

#### Damiano Testa (Apr 23 2021 at 13:31):

I have not managed to understand what the definition of bot is: I imagine that it is -infinity, but I really do not know...

#### Johan Commelin (Apr 23 2021 at 13:31):

So I would suggest that you first write those simp-lemmas, if they are missing.

#### Damiano Testa (Apr 23 2021 at 13:31):

ok, I will try. This might still be hard, since I have no idea how to work with bot...

#### Johan Commelin (Apr 23 2021 at 13:31):

So, hunt down the instance that gives you the addition (using widgets, eg)

#### Damiano Testa (Apr 23 2021 at 13:32):

I tried with widgets, but I only get to the "generic" instance.

#### Johan Commelin (Apr 23 2021 at 13:32):

What do you mean with that?

#### Damiano Testa (Apr 23 2021 at 13:32):

Anyway, I will try to prove the focused lemma that bot + .. = bot.

#### Johan Commelin (Apr 23 2021 at 13:33):

My guess is that \bot + x = \bot will be by cases x; refl

#### Damiano Testa (Apr 23 2021 at 13:33):

I mean that I have only gotten to seeing that with_bot ... = option ..., but I cannot find the addition

#### Damiano Testa (Apr 23 2021 at 13:33):

Ok, let me try with that: it might be enough!

#### Johan Commelin (Apr 23 2021 at 13:33):

Click on the + to get a widget for that, and then follow the instance chain.

#### Damiano Testa (Apr 23 2021 at 13:35):

I tried, I will try again, but, as you said, this works:

lemma bot_add {α : Type*} [add_comm_monoid α] (a : with_bot α) :
(⊥ + a : with_bot α) = ⊥ :=
begin
cases a;
refl,
end


thanks!

#### Damiano Testa (Apr 23 2021 at 13:36):

And then,

lemma bot_add_le {α : Type*} [add_comm_monoid α] [partial_order α]
{a b : α} (bc : (a : with_bot α) ≤ b) :
(⊥ + some a : with_bot α) ≤ ⊥ + some b :=


#### Johan Commelin (Apr 23 2021 at 13:36):

bot_add should be a simp-lemma

#### Damiano Testa (Apr 23 2021 at 13:38):

Ok, it is exactly what I needed, even though I asked something different! Thanks a lot for realizing what I should have asked and for answering it!

#### Johan Commelin (Apr 23 2021 at 13:39):

Still, I'm very surprised that these lemmas aren't there yet.

#### Eric Wieser (Apr 23 2021 at 13:40):

with_bot seems to be having an identity crisis about its simp-normal form

#### Damiano Testa (Apr 23 2021 at 13:40):

Also, you can weaken the hypotheses at least

lemma bot_add {α : Type*} [add_semigroup α] (a : with_bot α) :
(⊥ + a : with_bot α) = ⊥ :=
by cases a; refl


#### Eric Wieser (Apr 23 2021 at 13:40):

IMO the only lemmas we should have about none and some are "convert these to bot and coe"

#### Damiano Testa (Apr 23 2021 at 13:41):

Johan, is the issue that I should have add_comm first?

#### Johan Commelin (Apr 23 2021 at 13:41):

Nope, I just linked to the wrong variant.

#### Johan Commelin (Apr 23 2021 at 13:41):

bot_add is listed above it

#### Eric Wieser (Apr 23 2021 at 13:41):

I think we're missing

instance [has_add α] : has_add (with_bot α) := with_top.has_add


#### Eric Wieser (Apr 23 2021 at 13:42):

Which would then completely relax the requirements on that lemma

#### Damiano Testa (Apr 23 2021 at 13:42):

This also does not work:

import algebra.ordered_monoid

lemma add_bot {α : Type*} [add_semigroup α] (a : with_bot α) :
(a + ⊥ : with_bot α) = ⊥ :=
by simp


#### Eric Wieser (Apr 23 2021 at 13:42):

Yes, that's because as you remark the typeclass on the lemmas is wrong

#### Eric Wieser (Apr 23 2021 at 13:43):

So simp can't apply them there

#### Eric Wieser (Apr 23 2021 at 13:43):

@Alex J. Best, do you have any plans to pick back up your "needlessly strong typeclass" linter?

#### Damiano Testa (Apr 23 2021 at 13:44):

Ok, so, I will leave this be for the moment: I am already messed up with the order hierarchy and do not have the strength to pick this fight as well! I will make do with the lemma bot_add and will introduce more, as needed, now that I understand better what is going on!

#### Alex J. Best (Apr 23 2021 at 13:45):

@Eric Wieser yes, I intend to restart work on it very soon!

#### Kevin Buzzard (Apr 23 2021 at 18:16):

Eric Wieser said:

I think we're missing

instance [has_add α] : has_add (with_bot α) := with_top.has_add


This is just the sort of nonsense which leaks and causes trouble, isn't it? Why not just duplicate the proof?

#### Eric Wieser (Apr 23 2021 at 18:17):

Because every definition for with_bot is done that way

#### Eric Wieser (Apr 23 2021 at 18:19):

So my suggestion is just copying src#with_bot.add_monoid, whether or not what's currently done is actually a good idea

Last updated: Dec 20 2023 at 11:08 UTC