Zulip Chat Archive

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

lemma bot_add_le {α : Type*} [add_comm_monoid α] [partial_order α]
  {a b : α} (bc : (a : with_bot α)  b) :
  ( + some a : with_bot α)   + some b :=
begin
  admit,
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

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

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 :=
by simp [bot_add]

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.

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

https://leanprover-community.github.io/mathlib_docs/algebra/ordered_monoid.html#with_bot.add_bot

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