with_bot

Stream: new members

[Damiano Testa]

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]

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

[Johan Commelin]

So some a could be any term of with_bot

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

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]

So you can generalize the lemma

[Damiano Testa]

simp constantly fails...

[Johan Commelin]

There should be a simp lemma with_bot.some_eq_coe.

[Damiano Testa]

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]

so applying simp should change something?

[Johan Commelin]

Unless the lemma doesn't exist )-;

[Damiano Testa]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

There should be simp-lemmas for this.

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

What do you mean with that?

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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]

thanks!

[Damiano Testa]

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]

bot_add should be a simp-lemma

[Damiano Testa]

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]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Johan Commelin]

Nope, I just linked to the wrong variant.

[Johan Commelin]

bot_add is listed above it

[Eric Wieser]

I think we're missing

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

[Eric Wieser]

Which would then completely relax the requirements on that lemma

[Damiano Testa]

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]

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

[Eric Wieser]

So simp can't apply them there

[Eric Wieser]

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

[Damiano Testa]

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]

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

[Kevin Buzzard]

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]

Because every definition for with_bot is done that way

[Eric Wieser]

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