## Stream: triage

### Topic: PR #4273: feat(data/set/intervals/with_bot_top): lemmas a...

#### Random Issue Bot (Nov 03 2020 at 14:14):

Today I chose PR 4273 for discussion!

feat(data/set/intervals/with_bot_top): lemmas about I?? and with_top/bot
Created by @Yury G. Kudryashov (@urkud) on 2020-09-26
Labels: awaiting-author, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

#### Yury G. Kudryashov (Nov 03 2020 at 14:41):

For this PR we need to make with_top and with_bot irreducible.

#### Yury G. Kudryashov (Nov 03 2020 at 14:41):

If someone wants to help me with this refactor, tell me, please.

#### Yury G. Kudryashov (Nov 03 2020 at 14:42):

I started this in a branch but didn't fix all failures yet.

#### Kevin Buzzard (Nov 03 2020 at 15:12):

Which branch? I did this for with_zero and with_one and found it quite fun.

#### Kevin Buzzard (Nov 03 2020 at 15:12):

(I did a certain amount of cheating when I couldn't figure it out, e.g. making them locally reducible for a proof or two when I couldn't get to the bottom of a failure, but I'll try harder this time)

#### Yury G. Kudryashov (Nov 03 2020 at 15:24):

https://github.com/leanprover-community/mathlib/tree/irreducible-with-top

#### Yury G. Kudryashov (Nov 03 2020 at 15:24):

I'll merge master into this branch today

#### Kevin Buzzard (Nov 07 2020 at 20:19):

I have some time for this now. I got conditionally_complete_lattice compiling; you might want to take a look at this @Yury G. Kudryashov just to check that you don't think my methods are too crude. Temporarily making with_top/with_bot reducible sometimes fixes some errors and creates others. If I can't do this, I can't do cases on a : with_top X so I brutally apply the with_top.rec_top_coe recursor. Am I missing a trick?

#### Yury G. Kudryashov (Nov 07 2020 at 20:21):

Currently the main problem I see is that some algebraic instances don't work well unless I make both with_top and with_bot semireducible.

#### Yury G. Kudryashov (Nov 07 2020 at 20:22):

E.g., sometimes Lean can't unify two has_add instances on with_bot, one coming from has_add α, and another coming from add_monoid α via add_monoid (with_bot α).

#### Yury G. Kudryashov (Nov 07 2020 at 20:23):

I think that this bad; we should make with_top/with_bot semireducible only if we want to use functions and theorems about option.

#### Kevin Buzzard (Nov 07 2020 at 21:11):

I am working on ereal and it seems that there are two non-defeq orders on it, one coming from order_bot and another from the linear order. I was seeing the same issues in conditionally_complete_lattice.

#### Kevin Buzzard (Nov 07 2020 at 21:13):

I don't really understand what you're saying -- are you suggesting that this PR be abandoned? Do you think that we could do some clever priority changing to sort these issues out? (I think I'm seeing the same type of problem in the order hierarchy as you're seeing in the algebra hierarchy).

#### Kevin Buzzard (Nov 07 2020 at 21:25):

Hmm. I've just solved my lattice nondefeq order issue by writing

@[derive [linear_order, order_bot, order_top,
def ereal := with_top (with_bot ℝ)

local attribute [reducible] with_bot with_top


instead of making them reducible before letting the derive handler run.

#### Yury G. Kudryashov (Nov 07 2020 at 23:43):

We should change some instances so that Lean can match different has_adds without making with_bot and with_top locally semireducible.

#### Yury G. Kudryashov (Nov 07 2020 at 23:43):

BTW, you should make them semireducible, not reducible.

#### Yury G. Kudryashov (Nov 07 2020 at 23:44):

Otherwise Lean treat both of them as option α for the purpose of instance search.

#### Yury G. Kudryashov (Nov 07 2020 at 23:44):

And it can apply with_top instance to with_bot α.

#### Yury G. Kudryashov (Nov 07 2020 at 23:45):

E.g., I added some { zero := 0, add := (+) } to with_bot.add_monoid etc.

#### Yury G. Kudryashov (Nov 07 2020 at 23:45):

I thought that this will help but it doesn't. Probably we need to do the same with some with_top instances.

#### Kevin Buzzard (Nov 08 2020 at 00:39):

The semireducible (not reducible) trick has fixed the issues I was having with ereal -- thanks! I've also got ennreal compiling (by just making with_top semireducible at the top of the file and then irreducible at the bottom -- are you happy with this approach?).

Can you point me to a specific issue with addition so I can try and understand the problem better? I'm sure I'll run into one soon enough but I may as well try and understand what you think the big problem is.

#### Eric Wieser (Nov 08 2020 at 09:06):

I assume these types were irreducible before? If so, the instance resolution pain sounds like exactly the thing I was experiencing with ring instances on tensor_algebra (see the algebra.semiring_to_ring thread)

#### Kevin Buzzard (Nov 08 2020 at 12:08):

with_bot and with_top were defined as option and were probably the default reducibility setting which I think is semireducible. This enables people to abuse type equality (e.g. using option.some) which can cause problems later on (e.g. option leaking out). The idea is that if you make everything irreducible then people are forced to write more type correct code.

#### Yury G. Kudryashov (Nov 08 2020 at 17:59):

I have a deadline today. I'll look into this tomorrow. BTW, you don't need local attribute [irreducible] at the bottom. Lean forgets about local attribute [semireducible] once it leaves the current section/namespace/file anyway.

#### Kevin Buzzard (Nov 08 2020 at 18:10):

Oh of course! local :-)

No hurry.

#### Kevin Buzzard (Nov 16 2020 at 22:58):

Yury G. Kudryashov said:

E.g., sometimes Lean can't unify two has_add instances on with_bot, one coming from has_add α, and another coming from add_monoid α via add_monoid (with_bot α).

@Yury G. Kudryashov I have now experienced this first hand with data.polynomial.degree.basic. The instances are defeq but things like rw would fail anyway. I changed some rw to erw, added some refls etc and got the file compiling; see this commit (sorry about the instance on line 509, I was debugging and forgot to remove it). Are you suggesting that I should not persevere with this approach? Do you understand why these defeq instances can't be unified by rw?

#### Kevin Buzzard (Nov 16 2020 at 23:07):

The next file is data.polynomial.degree.trailing_degree which uses some : ℕ → with_top ℕ. I am a bit confused about what you want here. I had assumed we would make with_top.some but you didn't put it there. Do you have other plans? We have with_top.some_eq_coe and this is now "ill-typed" because it's option.some.

#### Damiano Testa (Nov 17 2020 at 05:22):

@Kevin Buzzard the file trailing_degree is one that I produced: I copied the degree file and did little more than sed to make the statements and proofs work. In particular, I do not know how to work with options: let me know if I can help, but I am not understanding much of this thread...

#### Kevin Buzzard (Nov 17 2020 at 07:49):

Don't worry Damiano, this isn't your problem. It's all about a redesign of with,_bot so it breaks a bunch of code and the question is how best to fix it, it's a design decision.

#### Random Issue Bot (Feb 04 2021 at 14:19):

Today I chose PR 4273 for discussion!

feat(data/set/intervals/with_bot_top): lemmas about I?? and with_top/bot
Created by @Yury G. Kudryashov (@urkud) on 2020-09-26
Labels: awaiting-author, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

#### Random Issue Bot (Apr 18 2021 at 14:22):

Today I chose PR 4273 for discussion!

feat(data/set/intervals/with_bot_top): lemmas about I?? and with_top/bot
Created by @Yury G. Kudryashov (@urkud) on 2020-09-26
Labels: awaiting-author, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

Last updated: May 09 2021 at 16:20 UTC