inhabited and nonempty instances

Stream: general

[Sebastien Gouezel]

It came up in #2720 that we don't have an instance saying that an add_comm_group is nonempty. Inhabiting basic classes like that can create problems: for instance, if you inhabit monoids by picking 1, and add_monoids by picking 0, then a ring would be inhabited both by 0 and 1, which can be bad. I would argue that, when there is a zero, it's always this one we should pick (although this is not completely obvious for groups with zeros). What do you think of adding the instances

instance has_zero.to_inhabited (α : Type*) [has_zero α] : inhabited α := ⟨0⟩
instance has_one.to_nonempty (α : Type*) [has_one α] : nonempty α := ⟨1⟩

Or should we replace the first one also with nonempty? Or drop this idea because it would lead to performance problems?

[Gabriel Ebner]

Conflicting nonempty instances are completely fine since nonempty is in Prop. I don't see any immediate problems with the inhabited by zero proposal either. Performance could be an issue, yes.

[Gabriel Ebner]

Why does #2720 require nonempty at all?

[Sebastien Gouezel]

In #2720, @Joseph Myers defines affine spaces, which are spaces on which a vector space acts freely and transitively. The empty space is endowed with a free and transitive action of any space, but it is not what you want, so requiring that an affine space is nonempty is natural. Then, when you want to show that a vector space is also an affine space for its action by translation on itself, you need to have available the instance saying that the vector space is nonempty.

[Mario Carneiro]

Conflicting inhabited instances can definitely be a problem. I don't think it is always guaranteed to be the case that 0 is the default element of every type that has a zero

[Mario Carneiro]

I recommend putting haveI : inhabited α := ⟨0⟩ whenever you need it in a proof

[Mario Carneiro]

or using a local instance

[Sebastien Gouezel]

I have prepared two branches, one using has_zero.to_inhabited and the other one has_zero.to_nonempty, to see if it breaks something or if compilation time increases. Let's wait for CI.

[Sebastien Gouezel]

Mario Carneiro said:

I don't think it is always guaranteed to be the case that 0 is the default element of every type that has a zero

In theory yes, but in practice I can't think of any example. If it works in 99,9% of the cases, we could enforce it as a rule.

[Mario Carneiro]

It seems like having these as local instances will solve most of the problems. Not all uses of inhabited have to do with algebra

[Mario Carneiro]

this looks like a very domain specific thing to do and I'd rather not add a global rule about it

[Mario Carneiro]

what is the default element of with_bot nat?

[Rob Lewis]

Another option if you have nonempty T and only need inhabited T within a proof, the tactic inhabit T will upgrade the instance locally.

[Mario Carneiro]

oh, does that tactic exist?

[Mario Carneiro]

If so it could do the same thing if it can prove T is a monoid or add_monoid

[Rob Lewis]

https://leanprover-community.github.io/mathlib_docs/tactics.html#inhabit

[Rob Lewis]

tactic#inhabit

[Kenny Lau]

tactic#inhabit

[Kenny Lau]

wait I thought those linkifiers thing need to start with a hashtag

[Rob Lewis]

lean#200

[Sebastien Gouezel]

The with_bot nat is a good example:

example : (has_zero.zero : with_top nat) ≠ default (with_top nat):= with_top.zero_ne_top

I am convinced that we should not have this as a global instance. In fact, I only care about nonempty, which can not create any theoretical problem. My only concern is that it could create performance problems: if you want to prove that a type is nonempty, and start looking for a zero, then there are so many ways to have a zero that it could lead to exponential blow-up very quickly. I guess these instances should be marked with pretty low priority to get a reasonable behavior.

[Gabriel Ebner]

You get the same performance issue with inhabited. And yes, they should have a low priority. (I believe we even have a linter that tells you that.)

[Yury G. Kudryashov]

Probably a better way to deal with the issue in #2720 is to require [nonempty] only where it is needed.

[Yury G. Kudryashov]

I mean, in most cases it doesn't matter if we call the empty set an affine space or not.

[Kevin Buzzard]

It comes up in the fundamental theorem relating torsors to group cohomology

[Yury G. Kudryashov]

Is it hard to add [nonempty] in this theorem?

[Kevin Buzzard]

I don't think so

[Sebastien Gouezel]

It feels strange that an affine space could be not in bijection with the underlying vector space, but I agree it is probably a good idea to remove it from the definition, and add it back when needed.

[Kevin Buzzard]

It feels strange that you can divide by 0, but we have to get used to these things ;-)

[Sebastien Gouezel]

Anyway, I have added the nonempty instances to the library, and it doesn't create bad performance problems: in a file importing a lot of things

lemma zou (α : Type*) [nondiscrete_normed_field α] : nonempty α :=
by apply_instance -- elaboration: tactic execution took 0ms

lemma zou2 (α : Type*) : nonempty α :=
by apply_instance -- fails, elaboration: tactic execution took 230ms

Since users could be surprised that Lean is unable to prove a ring is nonempty, I think we should include these instances. PR at #2743

[Sebastien Gouezel]

(In the case of zou2, if I activate the trace for class instances, the trace is too long, truncated at 262144 characters, as should be expected).

[Reid Barton]

Oh yes. Torsors are nonempty of course. They should extend nonempty.

[Reid Barton]

Well maybe not extend nonempty if that's problematic, just add it as a field I guess.

[Reid Barton]

Oh I see, it is there already :thumbs_up:

[Reid Barton]

I commented on the PR, but actually I think the best way to deal with #2720 is just to add nonempty P as a field of the structure.

[Joseph Myers]

If you allow affine spaces to be empty, and then probably allow affine subspaces of a nonempty affine space to be empty, you get things like equality for affine subspaces (given the bundled vector subspace, which seems natural to have) no longer being the same as equality for the set of points. Anything to do with dimension also gets complicated by having to allow dimension -1, which is the natural dimension for an empty space but no longer the same as the dimension of the underlying vector space. (You get complications either way, but I suspect "the intersection of two affine subspaces is only an affine subspace if nonempty" may be easier to deal with than the complications from allowing empty spaces and subspaces.)

[Reid Barton]

Hmm, so you are viewing an affine subspace as a "sub-(affine space)", that is, a subset which is a torsor for a subgroup of the original group, right? Then right, if the subset is empty (and if we allowed that), then the group could be anything.

[Sebastien Gouezel]

I agree that including nonemptyness as a field of the structure would solve everything, as it would avoid the typeclass inference issues.

[David Wärn]

Maybe if you want the empty space then you should define affine spaces in terms of "linear combinations where the coefficients sum to 1" rather than torsors

[Sebastien Gouezel]

No one wants the empty space, the question is rather the best way to avoid it :)

[Reid Barton]

I like this affine linear combination definition, but I'm not sure how it relates to additional structure on the vector space like a norm.

[David Wärn]

How about this? Define the vector space C (C for cone) spanned by an affine combination space A, left adjoint to the forgetful functor. Consider the kernel D (D for differences) of the linear map C -> k corresponding to the constant 1 map A -> k. Any point of A should naturally induce an affine isomorphism between D and A. Thus norms on D correspond to "Euclidean" distance functions on A. Presumably these distance functions can also be characterised by some sort of homogeneity and the parallelogram law