Zulip Chat Archive

Stream: general

Topic: deprecate with_zero.ordered_add_comm_monoid ??


view this post on Zulip Johan Commelin (May 27 2020 at 08:32):

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

view this post on Zulip Johan Commelin (May 27 2020 at 08:33):

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

view this post on Zulip Gabriel Ebner (May 27 2020 at 08:42):

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

view this post on Zulip Johan Commelin (May 27 2020 at 08:43):

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.

view this post on Zulip Gabriel Ebner (May 27 2020 at 08:45):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 09:11):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 09:13):

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

view this post on Zulip Johan Commelin (May 27 2020 at 09:16):

Ok, I'll leave it there


Last updated: May 14 2021 at 21:11 UTC