## 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,
{ cases le_total a c with hc hc,
{ 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 α]

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,
{ cases le_total a c with hc hc,
{ 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 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 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
{ cases le_total a c with hc hc,
{ 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
(@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: May 11 2021 at 00:31 UTC