Zulip Chat Archive

Stream: maths

Topic: nonempty


view this post on Zulip Patrick Massot (Mar 04 2019 at 19:12):

Is it evil to write

instance nonempty_of_zero {α : Type*} [has_zero α] : nonempty α := 0

instance nonempty_of_one {α : Type*} [has_one α] : nonempty α := 1

I doesn't seem to be there already, and that makes me nervous

view this post on Zulip Kevin Buzzard (Mar 04 2019 at 19:30):

The thing that makes me nervous is that you don't know which one Lean will find first in general, and the CS people will get edgy if something with a zero is proved non-empty by using a 1. I tried it with a 37 once and they didn't seem to like it. I guess 1 is a lot closer to zero but still I'm not sure they're going to be happy...

view this post on Zulip Chris Hughes (Mar 04 2019 at 19:35):

I PRed that once and was told it was evil.

view this post on Zulip Gabriel Ebner (Mar 04 2019 at 19:36):

It should be fine to have non-canonical instances here, since nonempty is a Prop. I wouldn't do this for inhabited, because then you run into all kinds of problems (which number is default ℕ..).

view this post on Zulip Mario Carneiro (Mar 04 2019 at 20:03):

What makes me nervous about this is it makes nonempty searches traverse the whole hierarchy

view this post on Zulip Patrick Massot (Mar 04 2019 at 20:54):

Ok, I feared something like this. What about defining a nonmepty instance for modules? vector spaces? please?

view this post on Zulip Mario Carneiro (Mar 04 2019 at 23:48):

I'm not saying you shouldn't do it, try it and find out if it's a problem

view this post on Zulip Patrick Massot (Feb 08 2020 at 21:22):

I just bumped mathlib in the perfectoid project and I really don't like https://github.com/leanprover-community/mathlib/pull/1954. It makes every statement ugly to save a couple of keystrokes in proofs. I know I had very little time for PR review since Christmas, but that PR was really game changing and was merged in one day.

view this post on Zulip Patrick Massot (Feb 08 2020 at 21:24):

I think readability of statements is really important, even when proofs are unreadable.

view this post on Zulip Patrick Massot (Feb 08 2020 at 21:32):

Also, it would be nice to have a log of breaking changes. Currently it's pretty painful to find why code is no longer working. That nonempty thing is obviously breaking lots of proofs, but now I'm chasing what happened to set.pointwise_mul_action.

view this post on Zulip Yury G. Kudryashov (Feb 08 2020 at 22:42):

I'm sorry for breaking your code. After reaction to #1779 I assumed that migration from ≠∅ to s.nonempty would be a desired change. If needed, I can revert everything back to ≠∅. Though I prefer the s.nonempty version, this is not a strong preference.
Let's also wait at least for @Floris van Doorn and @Sebastien Gouezel who approved this PR.

view this post on Zulip Yury G. Kudryashov (Feb 08 2020 at 23:09):

As for pointwise_mul_action, see #1925

view this post on Zulip Sebastien Gouezel (Feb 09 2020 at 08:16):

I think the move to nonempty was an excellent move. It takes some time to find the good abstractions, but once we have them we should definitely use them! Before, the fact that a set was nonempty could be expressed in three ways ((h : s ≠ ∅), or (h : ∃ x, x ∈ s) or (x : α) (h : x ∈ s)) and the three of them were used in some places in the library, making it necessary to jump through hoops when one needed one but the theorems were formulated with another one. With a standard way to express things and a nice API, everything becomes much neater. We don't have a word "pythonic" for Lean, but if we had one it would probably apply to this nonempty construct.

Of course, it is really bad that the change broke your code. To avoid this kind of bitrot, a solution would be to put the perfectoid project in the archive subdirectory of mathlib, so that PRs breaking your code would also have to fix it before getting merged. This is the policy with the AFP in Isabelle, and it works extremely well. I don't know if this is the way archive has been envisioned, though. Any thoughts?

view this post on Zulip Patrick Massot (Feb 09 2020 at 09:10):

Thanks Yury and Sébastien. I should have separated more clearly the different issues. My main points were:

  • this is a pretty drastic change that could have been discussed more (but of course it's difficult in a context where people's availability is very changing),

view this post on Zulip Patrick Massot (Feb 09 2020 at 09:11):

  • this makes statement less readable, so it should require extra argumentation

view this post on Zulip Patrick Massot (Feb 09 2020 at 09:12):

The point about the perfectoid code being broken is much less important (although it certainly participated in getting me to write a angry message, sorry about that).

view this post on Zulip Patrick Massot (Feb 09 2020 at 09:13):

The main problem about perfectoid code is our huge backlog of things that should be PRed to mathlib. My work yesterday aimed at bringing the project up to date with mathlib to resume the PR effort.

view this post on Zulip Patrick Massot (Feb 09 2020 at 09:45):

All that being said, I'm not really asking to revert that nonempty change. Let's add this to the huge pile of things that should improve in proofs assistants (to get both readable statements and good api). We can even tag this as :four_leaf_clover:

view this post on Zulip Patrick Massot (Feb 09 2020 at 09:46):

The pointwise_mul_action is much more tricky. It touches an area of mathlib that has always been very brittle.

view this post on Zulip Patrick Massot (Feb 09 2020 at 09:47):

Can @Jean Lo or anyone else who likes type class inference failure debug the following:

import algebra.pointwise
import ring_theory.algebra

local attribute [instance] set.smul_set_action

variables (R : Type*) [comm_ring R]

variables (A : Type*) [ring A] [algebra R A]

example : mul_action R (set A) :=
by apply_instance -- works

variables (B : Type*) [comm_ring B] [algebra R B]

example : mul_action R (set B) :=
by apply_instance -- fails

view this post on Zulip Patrick Massot (Feb 09 2020 at 09:53):

To be clear: in both cases the expected answer is the new set.smul_set_action, and both used to work before that change.

view this post on Zulip Chris Hughes (Feb 09 2020 at 10:29):

Increasing the instance_max_depth to 34 makes it work. The first instance requires a depth of 28 to make it work. I guess the comm_ring just made the search slightly deeper.

view this post on Zulip Patrick Massot (Feb 09 2020 at 16:38):

Thank you very much Chris!

view this post on Zulip Floris van Doorn (Feb 10 2020 at 02:08):

I did not consider the desiderata of readable theorem statements. It is indeed true that s.nonempty is a bit harder to read than s ≠ ∅.
I do still like nonempty better. Being able to do cases on this hypothesis to get an actual element is nice (and the readability is not that bad(?)).
I could wait longer to merge big PRs like that. However, I'm afraid that will result in more work for the PR author, which will have to fix merge conflicts.


Last updated: May 12 2021 at 07:17 UTC