Sebastien Gouezel (May 19 2020 at 07:28):
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
add_monoids by picking
0, then a ring would be inhabited both by
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 (May 19 2020 at 07:33):
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 (May 19 2020 at 07:34):
Why does #2720 require
nonempty at all?
Sebastien Gouezel (May 19 2020 at 07:38):
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 (May 19 2020 at 07:40):
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 (May 19 2020 at 07:42):
I recommend putting
haveI : inhabited α := ⟨0⟩ whenever you need it in a proof
Mario Carneiro (May 19 2020 at 07:43):
or using a local instance
Sebastien Gouezel (May 19 2020 at 07:55):
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 (May 19 2020 at 07:56):
Mario Carneiro said:
I don't think it is always guaranteed to be the case that
0is 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 (May 19 2020 at 07:56):
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 (May 19 2020 at 07:58):
this looks like a very domain specific thing to do and I'd rather not add a global rule about it
Mario Carneiro (May 19 2020 at 07:59):
what is the default element of
Rob Lewis (May 19 2020 at 08:00):
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 (May 19 2020 at 08:00):
oh, does that tactic exist?
Mario Carneiro (May 19 2020 at 08:01):
If so it could do the same thing if it can prove T is a monoid or add_monoid
Rob Lewis (May 19 2020 at 08:02):
Rob Lewis (May 19 2020 at 08:04):
Kenny Lau (May 19 2020 at 08:05):
Kenny Lau (May 19 2020 at 08:05):
wait I thought those linkifiers thing need to start with a hashtag
Rob Lewis (May 19 2020 at 08:06):
Sebastien Gouezel (May 19 2020 at 08:07):
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 (May 19 2020 at 08:11):
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 (May 19 2020 at 09:34):
Probably a better way to deal with the issue in #2720 is to require
[nonempty] only where it is needed.
Yury G. Kudryashov (May 19 2020 at 09:35):
I mean, in most cases it doesn't matter if we call the empty set an affine space or not.
Kevin Buzzard (May 19 2020 at 09:49):
It comes up in the fundamental theorem relating torsors to group cohomology
Yury G. Kudryashov (May 19 2020 at 09:54):
Is it hard to add
[nonempty] in this theorem?
Kevin Buzzard (May 19 2020 at 10:01):
I don't think so
Sebastien Gouezel (May 19 2020 at 10:01):
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 (May 19 2020 at 10:04):
It feels strange that you can divide by 0, but we have to get used to these things ;-)
Sebastien Gouezel (May 19 2020 at 10:12):
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 (May 19 2020 at 10:14):
(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 (May 19 2020 at 10:36):
Oh yes. Torsors are nonempty of course. They should extend
Reid Barton (May 19 2020 at 10:39):
Well maybe not
extend nonempty if that's problematic, just add it as a field I guess.
Reid Barton (May 19 2020 at 10:44):
Oh I see, it is there already :thumbs_up:
Reid Barton (May 19 2020 at 10:50):
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 (May 19 2020 at 10:53):
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 (May 19 2020 at 11:05):
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 (May 19 2020 at 11:45):
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 (May 19 2020 at 12:36):
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 (May 19 2020 at 12:37):
No one wants the empty space, the question is rather the best way to avoid it :)
Reid Barton (May 19 2020 at 13:07):
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 (May 19 2020 at 14:55):
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
Last updated: May 16 2021 at 20:13 UTC