Zulip Chat Archive

Stream: new members

Topic: nat as a canonically_linear_ordered_add_monoid


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

Eric Wieser (Feb 10 2021 at 01:19):

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

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?

Yakov Pechersky (Feb 10 2021 at 01:20):

And if so, why is nat not a canonically_linear_ordered_add_monoid?

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

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?

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...

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.

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?

Yakov Pechersky (Feb 10 2021 at 01:38):

Windows, using via WSL

Yakov Pechersky (Feb 10 2021 at 01:39):

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

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.

Yakov Pechersky (Feb 10 2021 at 01:45):

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

Yakov Pechersky (Feb 10 2021 at 01:45):

In any case: #6144

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.

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

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?

Eric Wieser (Feb 10 2021 at 08:02):

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

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

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.

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.

Rémy Degenne (Feb 10 2021 at 08:30):

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

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).

Eric Wieser (Feb 10 2021 at 08:56):

Can you make a branch to demo the problem?

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.

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.

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.

Eric Wieser (Feb 10 2021 at 11:21):

branch#ennreal_lattice_issue

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.

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: Dec 20 2023 at 11:08 UTC