nonempty

Stream: maths

[Patrick Massot]

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

[Kevin Buzzard]

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

[Chris Hughes]

I PRed that once and was told it was evil.

[Gabriel Ebner]

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 ℕ..).

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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.

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

As for pointwise_mul_action, see #1925

[Sebastien Gouezel]

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?

[Patrick Massot]

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),

[Patrick Massot]

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

[Patrick Massot]

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).

[Patrick Massot]

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.

[Patrick Massot]

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:

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Chris Hughes]

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.

[Patrick Massot]

Thank you very much Chris!

[Floris van Doorn]

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.