deprecate with_zero.ordered_add_comm_monoid ??

Stream: general

[Johan Commelin]

Is it ok if I move this to deprecated?

/--
If `0` is the least element in `α`, then `with_zero α` is an `ordered_add_comm_monoid`.
-/
def ordered_add_comm_monoid [ordered_add_comm_monoid α]
  (zero_le : ∀ a : α, 0 ≤ a) : ordered_add_comm_monoid (with_zero α) :=
begin
  suffices, refine {
    add_le_add_left := this,
    ..with_zero.partial_order,
    ..with_zero.add_comm_monoid, .. },
  { intros a b c h,
    have h' := lt_iff_le_not_le.1 h,
    rw lt_iff_le_not_le at ⊢,
    refine ⟨λ b h₂, _, λ h₂, h'.2 $ this _ _ h₂ _⟩,
    cases h₂, cases c with c,
    { cases h'.2 (this _ _ bot_le a) },
    { refine ⟨_, rfl, _⟩,
      cases a with a,
      { exact with_bot.some_le_some.1 h'.1 },
      { exact le_of_lt (lt_of_add_lt_add_left' $
          with_bot.some_lt_some.1 h), } } },
  { intros a b h c ca h₂,
    cases b with b,
    { rw le_antisymm h bot_le at h₂,
      exact ⟨_, h₂, le_refl _⟩ },
    cases a with a,
    { change c + 0 = some ca at h₂,
      simp at h₂, simp [h₂],
      exact ⟨_, rfl, by simpa using add_le_add_left' (zero_le b)⟩ },
    { simp at h,
      cases c with c; change some _ = _ at h₂;
        simp [-add_comm] at h₂; subst ca; refine ⟨_, rfl, _⟩,
      { exact h },
      { exact add_le_add_left' h } } }
end

[Johan Commelin]

I'm pretty sure it's not used in mathlib, and I get the shivers by simply looking at the type of this def...

[Gabriel Ebner]

This looks perfectly reasonable to me. What is wrong with it?

[Johan Commelin]

Well, your type has a zero, and then you add a new zero to it. That's something that shouldn't be encouraged, I think.

[Gabriel Ebner]

Oh, I missed that. Then let's get rid of it!

[Mario Carneiro]

The point is to provide sufficient conditions on when with_zero A is an ordered_add_comm_monoid

[Mario Carneiro]

yes it's a weird theorem, but it's also a hole-filling theorem. I've said this before but we should have theorems about the pairwise interaction of all concepts in mathlib

[Johan Commelin]

Ok, I'll leave it there