Zulip Chat Archive

Stream: new members

Topic: nat as a canonically_linear_ordered_add_monoid


view this post on Zulip Yakov Pechersky (Feb 10 2021 at 01:13):

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

view this post on Zulip Eric Wieser (Feb 10 2021 at 01:19):

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

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 01:20):

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

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 01:20):

And if so, why is nat not a canonically_linear_ordered_add_monoid?

view this post on Zulip Eric Wieser (Feb 10 2021 at 01:23):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 01:28):

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?

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 01:32):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 01:34):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 01:36):

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?

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 01:38):

Windows, using via WSL

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 01:39):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 01:42):

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.

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 01:45):

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

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 01:45):

In any case: #6144

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 03:49):

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.

view this post on Zulip Eric Wieser (Feb 10 2021 at 07:34):

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

view this post on Zulip Rémy Degenne (Feb 10 2021 at 08:00):

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?

view this post on Zulip Eric Wieser (Feb 10 2021 at 08:02):

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

view this post on Zulip Eric Wieser (Feb 10 2021 at 08:03):

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

view this post on Zulip Rémy Degenne (Feb 10 2021 at 08:06):

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.

view this post on Zulip Rémy Degenne (Feb 10 2021 at 08:28):

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.

view this post on Zulip Rémy Degenne (Feb 10 2021 at 08:30):

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

view this post on Zulip Rémy Degenne (Feb 10 2021 at 08:51):

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

view this post on Zulip Eric Wieser (Feb 10 2021 at 08:56):

Can you make a branch to demo the problem?

view this post on Zulip Rémy Degenne (Feb 10 2021 at 09:12):

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.

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 09:17):

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

view this post on Zulip Rémy Degenne (Feb 10 2021 at 09:58):

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.

view this post on Zulip Eric Wieser (Feb 10 2021 at 11:21):

branch#ennreal_lattice_issue

view this post on Zulip Rémy Degenne (Feb 10 2021 at 12:48):

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

view this post on Zulip Rémy Degenne (Feb 10 2021 at 12:49):

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


Last updated: May 11 2021 at 00:31 UTC