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

Stream: triage

[Random Issue Bot]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(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]

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

[Yury G. Kudryashov]

I'll merge master into this branch today

[Kevin Buzzard]

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]

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]

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

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]

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]

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

@[derive [linear_order, order_bot, order_top,
  has_Sup, has_Inf, complete_lattice, has_add]]
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]

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]

BTW, you should make them semireducible, not reducible.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

And it can apply with_top instance to with_bot α.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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]

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]

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]

Oh of course! local :-)

[Kevin Buzzard]

No hurry.

[Kevin Buzzard]

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]

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]

@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]

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]

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]

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]

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

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