nat as a canonically_linear_ordered_add_monoid

Stream: new members

[Yakov Pechersky]

I was writing the following:

lemma nat.min_add_distrib (a b c : ℕ) :
  min a (b + c) = min a (min a b + min a c) :=
begin
  cases le_total a b with hb hb,
  { simp [hb, le_add_right] },
  { cases le_total a c with hc hc,
    { simp [hc, le_add_left] },
    { simp [hb, hc] } }
end

and thought to generalize. But here is a #mwe of variants of the proof with different generalizations. What makes the nat one work, and what's wrong with the broken ones?

import data.nat.cast

variables {α β : Type*} [canonically_linear_ordered_add_monoid α]
  [canonically_ordered_add_monoid β] [linear_order β]

lemma min_add_distrib (a b c : α) :
  min a (b + c) = min a (min a b + min a c) :=
begin
  cases le_total a b with hb hb,
  { simp [hb, le_add_right] },
  { cases le_total a c with hc hc,
    { simp [hc, le_add_left] },
    { simp [hb, hc] } }
end

lemma min_add_distrib_rw (a b c : α) :
  min a (b + c) = min a (min a b + min a c) :=
begin
  cases le_total a b with hb hb,
  { rw [min_eq_left hb, min_eq_left, min_eq_left],
    { exact le_add_right (le_refl a) },
    { exact le_add_right hb } },
  { cases le_total a c with hc hc,
    { rw [min_eq_left, min_eq_left],
      { rw [min_eq_left hc],
        exact le_add_left (le_refl a) },
      { exact le_add_left hc } },
    { rw [min_eq_right hc, min_eq_right hb] } }
end

lemma min_add_distrib_broken (a b c : β) :
  min a (b + c) = min a (min a b + min a c) :=
begin
  cases le_total a b with hb hb,
  { rw [min_eq_left hb, min_eq_left, min_eq_left],
    { exact le_add_right (le_refl a) }, -- breaks here. different orders?
    { exact le_add_right hb } },
  { cases le_total a c with hc hc,
    { rw [min_eq_left, min_eq_left],
      { rw [min_eq_left hc],
        exact le_add_left (le_refl a) },
      { exact le_add_left hc } },
    { rw [min_eq_right hc, min_eq_right hb] } }
end

lemma nat.min_add_distrib_broken (a b c : ℕ) :
  min a (b + c) = min a (min a b + min a c) :=
min_add_distrib a b c -- does not work

lemma nat.min_add_distrib (a b c : ℕ) :
  min a (b + c) = min a (min a b + min a c) :=
begin
  cases le_total a b with hb hb, -- same proof as above
  { simp [hb, le_add_right] },
  { cases le_total a c with hc hc,
    { simp [hc, le_add_left] },
    { simp [hb, hc] } }
end

[Eric Wieser]

Aren't you putting two different preorders on \B, since both typeclasses have the same base?

[Yakov Pechersky]

Yes, that's what breaks it. But what makes the nat version work then? The fact that the underlying order is the same?

[Yakov Pechersky]

And if so, why is nat not a canonically_linear_ordered_add_monoid?

[Eric Wieser]

Yes, the elaborator(?) will deduce the two preorder structures are the same for nat, by unfolding both

[Bryan Gin-ge Chen]

docs#canonically_linear_ordered_add_monoid doesn't have an "instances" section at all. Maybe we just haven't gotten around to declaring any in mathlib yet?

[Yakov Pechersky]

I'd be happy to add it -- but my vscode decided to break all the webview plugins, including the Lean one...

[Bryan Gin-ge Chen]

Heh, it doesn't look like any instances were added when the class was added in #3335, nor in any of the commits afterwards.

[Bryan Gin-ge Chen]

Yakov Pechersky said:

I'd be happy to add it -- but my vscode decided to break all the webview plugins, including the Lean one...

I updated VS Code a bit earlier today but I haven't seen any breakage yet. What OS are you on?

[Yakov Pechersky]

Windows, using via WSL

[Yakov Pechersky]

Git Graph is also not working, which suggests a webview problem

[Bryan Gin-ge Chen]

Ah, I see. I couldn't find any relevant-looking recent issues at https://github.com/microsoft/vscode/issues so it might be worth reporting there.

[Yakov Pechersky]

A lot of older issues referencing this from around June though =C

[Yakov Pechersky]

In any case: #6144

[Bryan Gin-ge Chen]

What's the best solution for this sort of thing? I just made a suggestion in another of Yakov's PRs which ran into the same problem, where now the instances for linear_ordered_comm_monoid_with_zero and ordered_cancel_add_comm_monoid have orders that don't necessarily agree.

[Eric Wieser]

Any time you need the properties of two different typeclasses with the same base, you have to introduce a third typeclass extending both

[Rémy Degenne]

I had a branch in which I added a canonically_linear_ordered_add_monoid instance to nnreal, which works fine, as well as
instance with_top.canonically_linear_ordered_add_monoid as done in #6144, with the idea of applying that to ennreal. But then the orders on ennreal conflict. ennreal would need a typeclass which is also a complete lattice (if I remember correctly). I was hoping for another solution because I did not want to add a complete_canonically_linear_ordered_add_monoid which would only apply to ennreal. Eric, you say that adding that other class is the only way?

[Eric Wieser]

Two different typeclasses which provide the same order on the same type don't conflict

[Eric Wieser]

It's only when you define a lemma taking two typeclasses that _could_ conflict that you have a problem, because without a concrete type to look at, the two instances can't just be unfolded and checked for equality

[Rémy Degenne]

Ok. Then I don't remember it correctly, or don't describe it correctly. I think it had to do with the lattice, which can come from canonically_linear_ordered_monoid.semilattice_sup_bot or from the complete_linear_order on ennreal, but I'll test that branch again rather than conjecture based on old impressions.

[Rémy Degenne]

When I add [derive canonically_linear_ordered_add_monoid] to ennreal (without removing/changing any of the other derived instances), the lemma diam_triple in topology/metric_space/emetric_space.lean fails, because of ennreal.sup_eq_max. The issue seems to be that there are two different has_sup:

invalid type ascription, term has type
  @eq ennreal
    (@has_sup.sup ennreal
       (@semilattice_sup.to_has_sup ennreal
          (@semilattice_sup_bot.to_semilattice_sup ennreal
             (@canonically_linear_ordered_add_monoid.semilattice_sup_bot ennreal
                ennreal.canonically_linear_ordered_add_monoid)))
       (@has_edist.edist α (@emetric_space.to_has_edist α _inst_1) x y)
       (@has_edist.edist α (@emetric_space.to_has_edist α _inst_1) x z))
    (@max ennreal
       (@conditionally_complete_linear_order.to_linear_order ennreal
          (@conditionally_complete_linear_order_of_complete_linear_order ennreal ennreal.complete_linear_order))
       (@has_edist.edist α (@emetric_space.to_has_edist α _inst_1) x y)
       (@has_edist.edist α (@emetric_space.to_has_edist α _inst_1) x z))
but is expected to have type
  @eq ennreal
    (@has_sup.sup ennreal
       (@semilattice_sup.to_has_sup ennreal
          (@semilattice_sup_bot.to_semilattice_sup ennreal
             (@semilattice_sup_bot_of_bounded_lattice ennreal
                (@complete_lattice.to_bounded_lattice ennreal
                   (@complete_linear_order.to_complete_lattice ennreal ennreal.complete_linear_order)))))
       (@has_edist.edist α (@emetric_space.to_has_edist α _inst_1) x y)
       (@has_edist.edist α (@emetric_space.to_has_edist α _inst_1) x z))
    (@max ennreal
       (@conditionally_complete_linear_order.to_linear_order ennreal
          (@conditionally_complete_linear_order_of_complete_linear_order ennreal ennreal.complete_linear_order))
       (@has_edist.edist α (@emetric_space.to_has_edist α _inst_1) x y)
       (@has_edist.edist α (@emetric_space.to_has_edist α _inst_1) x z))

Is it true that the with_top of a canonically_linear_ordered_add_monoid is a complete_lattice? We could remove the [derive complete_linear_order] on ennreal and it would remove the issue.

[Rémy Degenne]

It is certainly a bounded lattice, but I don't know about complete

[Rémy Degenne]

and the answer is no, if I am not mistaken. A counterexample would be the non-negative rational numbers (with top).

[Eric Wieser]

Can you make a branch to demo the problem?

[Rémy Degenne]

I created the branch ennreal_lattice_issue, in which I started from #6144 and added a canonically_linear_ordered_add_monoid instance to ennreal. It is still building so I don't know yet if the issue I am trying to replicate is visible. I'll update this thread when it is done.

[Yakov Pechersky]

Yes, that derive was reverted in my last commit, because of this exact issue. You identified the lemma that breaks.

[Rémy Degenne]

The branch ennreal_lattice_issue finished building (the build failed). There is an issue with the use of ennreal.sup_eq_max in the proof of diam_triple in topology/metric_space/emetric_space.

[Eric Wieser]

branch#ennreal_lattice_issue

[Rémy Degenne]

I think that I found a fix: removing instance canonically_linear_ordered_monoid.semilattice_sup_bot.

[Rémy Degenne]

I am waiting for the build to succeed, to be sure that it did not break anything else.