saturating addition on the bottom

Stream: Is there code for X?

[Yakov Pechersky]

Is there an existing proof for the following?

import data.polynomial.monic

example (m n : with_bot ℕ) :
  m + n = ⊥ ↔ m = ⊥ ∨ n = ⊥ :=
begin
  split,
  { sorry },
  { rintro (rfl|rfl);
    simp }
end

[Yaël Dillies]

Wait, is this how addition is defined on with_bot ℕ?

[Yakov Pechersky]

with_bot nat is saturating on the bottom, according to

@[simp] lemma bot_add [ordered_add_comm_monoid α] (a : with_bot α) : ⊥ + a = ⊥ := rfl

@[simp] lemma add_bot [ordered_add_comm_monoid α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl

[Yakov Pechersky]

Did you think it was a new additive identity?

[Yaël Dillies]

No, I just never encountered it.

[Yaël Dillies]

Here's my proof of your sorry

import data.polynomial.monic

example (m n : with_bot ℕ) :
  m + n = ⊥ ↔ m = ⊥ ∨ n = ⊥ :=
begin
  split,
  { cases m,
    { exact λ _, or.inl rfl },
    cases n,
    { exact λ _, or.inr rfl },
    exact λ h, (option.some_ne_none _ h).elim },
  { rintro (rfl | rfl);
    simp }
end

[Sebastien Gouezel]

lemma add_eq_bot [add_monoid α] {a b : with_bot α} : a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥ :=
with_top.add_eq_top

[Yakov Pechersky]

Ew, defeq abuse :upside_down:

[Yakov Pechersky]

#8474

[Eric Wieser]

I like Sebastien's proof, it's like proving infi lemmas using supr lemmas

[Eric Wieser]

And probably exposes a bunch of missing lemmas about with_bot

[Yakov Pechersky]

I proved it using API that I added in, which copied most of the syntax from existing with_top lemmas.

[Kevin Buzzard]

When I was working with ereal I noticed that because both with_bot and with_top had saturating addition for the extreme element they were adding, the value of bot+top in ereal depended on which one the implementation added last. When I was working on ereal I found this so mathematically unappealing that IIRC I didn't define addition at all

[Eric Wieser]

I mean, what value did you want bot+top to have?

[Sebastien Gouezel]

I needed more algebraic structure on ereal for the Vitali-Caratheodory theorem, so I defined addition and multiplication there. With bot + top = top, because top is in general more interesting than bot. ereal is even a linear_ordered_add_comm_monoid_with_top and a comm_monoid_with_zero.

[Kevin Buzzard]

I feel really vindicated by this! I remember just refusing to add addition, I said that the PR had all you needed to make any definition of addition you want but I didn't want to make the decision myself because I did not need it for my application.

[Kevin Buzzard]

IIRC the definition was with_bot (with_top \R) so you would have been stuck with the bad addition I think if I'd just derived it and made some crappy API

[Eric Wieser]

src#ereal

[Eric Wieser]

As it happens, the addition _is_ just @[derive]d, but from with_top (with_bot ℝ) not with_bot (with_top ℝ)