Zulip Chat Archive
Stream: mathlib4
Topic: data.set.intervals.basic
Scott Morrison (Dec 14 2022 at 23:13):
We had a race condition: https://github.com/leanprover-community/mathlib4/pull/1034 and https://github.com/leanprover-community/mathlib4/pull/1033 a mere two minutes apart.
@Winston Yin, @Arien Malec, would either or both of you have a change to triage these into a single PR shortly? Perhaps one can just be closed, or you can move some pieces from one to the other if appropriate.
Arien Malec (Dec 14 2022 at 23:14):
Let me check who's farther...
Arien Malec (Dec 14 2022 at 23:14):
most likely @Winston Yin
Winston Yin (Dec 14 2022 at 23:14):
@Arien Malec I've ported till line 1149
Arien Malec (Dec 14 2022 at 23:15):
I mostly did the grunt work of cleaning up obvious fixes -- I'll close mine...
Arien Malec (Dec 14 2022 at 23:16):
@Winston Yin if you want to focus on the broken proofs I'm happy to repeat the grunt work on your branch.
Winston Yin (Dec 14 2022 at 23:16):
Sure. I'm trying to rewrite all the tauto proofs
Winston Yin (Dec 14 2022 at 23:17):
Sorry that you're doing repetitive work!
David Renshaw (Dec 14 2022 at 23:18):
FWIW, I'm in the middle of porting tauto.
Winston Yin (Dec 14 2022 at 23:20):
How long do you anticipate that to take? If Data.Set.Intervals.Basic is not in the way of everything, I can leave the tautos in for now
David Renshaw (Dec 14 2022 at 23:21):
I hope it should just be a few more days, but it's hard to say.
David Renshaw (Dec 14 2022 at 23:21):
If it's going to accelerate things, I might consider trying to land an incomplete less-optimized version.
Arien Malec (Dec 14 2022 at 23:24):
@Winston Yin don't touch anything that's not tauto and we'll be good rn.
Winston Yin (Dec 14 2022 at 23:24):
What does it mean "anything that's not tauto"?
Winston Yin (Dec 14 2022 at 23:24):
There are some broken proofs having nothing to do with tauto
Arien Malec (Dec 14 2022 at 23:26):
e.g., unknown h.trans or simp [Ici]
Winston Yin (Dec 14 2022 at 23:27):
Actually I have only another half hour or so to work on this. Feel free to take over the PR in 30 min
Arien Malec (Dec 14 2022 at 23:28):
OK -- & just pushed some super simple fixes.
Winston Yin (Dec 15 2022 at 03:03):
@David Renshaw I've replaced all the tauto in this file with simp proofs, with a porting note to restore them back to tauto when your work is done
Winston Yin (Dec 15 2022 at 03:06):
I mean, we don't have to restore the tautos but it's good for testing and examples of its use
Ruben Van de Velde (Dec 15 2022 at 06:56):
David Renshaw said:
If it's going to accelerate things, I might consider trying to land an incomplete less-optimized version.
Are you saying your current code is incomplete or slow or both? Because I think a complete but slow implementation would be very helpful to land asap
David Renshaw (Dec 15 2022 at 14:06):
Yeah, I have a working implementation that does not yet handle relations with symmetry (though should automatically pick up that ability to some extent once solve_by_elim does). I'll work on putting up a PR for that.
mathlib3 tauto uses a fancy union-find data structure to try to apply symmetry as efficiently as possible. I'm finding what look like some bugs in it: https://github.com/leanprover-community/mathlib/pull/17958 . I think it makes sense for mathlib4's first version of tauto to not bother with this stuff yet.
David Renshaw (Dec 16 2022 at 16:13):
https://github.com/leanprover-community/mathlib4/pull/1081
Last updated: Dec 20 2023 at 11:08 UTC