unique from empty

Stream: Is there code for X?

[Yakov Pechersky]

Do we have something that can give:

example : option (fin 0) ≃ unit := sorry

Something like pi.unique_of_empty but saying that unique [option α] when α ≃ empty.

[Floris van Doorn]

I guess you already know about docs#equiv_punit_of_unique? The other part seems like it's missing, but is very easy.

[Mario Carneiro]

the other direction sounds like the composition of two lemmas, equivs preserve unique and unique pempty

[Mario Carneiro]

I wouldn't make that into one lemma unless it's one half of an iff statement

[Floris van Doorn]

I think (\a -> false) -> unique (option \a) is a reasonable lemma to have.

[Mario Carneiro]

that could also be one half of an iff statement

[Floris van Doorn]

Honestly, I feel like we should add [is_empty \a] as a typeclass

[Johan Commelin]

I'm a fan

[Mario Carneiro]

that works for me

[Mario Carneiro]

there aren't that many instances but there are at least 2 or 3

[Johan Commelin]

We already have subsingleton, unique, nonempty and nontrivial. It's only reasonable to also have is_empty.

[Mario Carneiro]

Of course you have to keep in mind that because of the @[class] def thing this might not be easier to use than A -> false

[Johan Commelin]

empty, pempty, {x // x \in \empty}, false, prime_spectrum punit

[Mario Carneiro]

fin 0, A -> false where nonempty A

[Floris van Doorn]

↥∅ for ∅ in various types

[Floris van Doorn]

Mario Carneiro said:

A -> false where nonempty A

A -> Bwhere nonempty A and is_empty B :)

[Johan Commelin]

I think we have convincingly, and even constructively! proven Marios conjecture that there are at least 2 or 3 examples (-;

[Mario Carneiro]

lean has too many ways to say nothing :)

[Johan Commelin]

It's a hard problem! If you can fix it, I guess you solved the "canonical isomorphism" problem (-;

[Gabriel Ebner]

Floris van Doorn said:

Mario Carneiro said:

A -> false where nonempty A

A -> Bwhere nonempty A and is_empty B :)

I think you can drop the nonempty A assumption here.

[Floris van Doorn]

I don't think so

[Mario Carneiro]

false -> false is true

[Gabriel Ebner]

Oops. You're right of course.

[Johan Commelin]

If we introduce this class, there will be 37 files (or more) where we can replace (p)empty using this class.

[Mario Carneiro]

not all of those would necessarily be a good idea

[Mario Carneiro]

in particular we don't want algebraic classes for these types just because they are empty

[Johan Commelin]

Sure, but we prove things about mv_polynomial pempty R and also about mv_polynomial (fin 0) R

[Mario Carneiro]

certainly if be have any duplicated lemmas then that's a good candidate, but if you want the initial object of Set to inhabit a typeclass you probably don't want that to be generic

[Mario Carneiro]

docs#equiv.prod_empty looks like it could be generalized, although prod_punit isn't

[Kevin Buzzard]

When I was proving some instances of free_abelian_group I proved free_abelian_group pempty ≃+ unit and free_abelian_group punit ≃+ ℤ and then in the PR process Eric said I would be better off proving punit_equiv (T : Type*) [unique T] : free_abelian_group T ≃+ ℤ and pempty_unique : unique (free_abelian_group pempty). This does seem like a natural extension of this. The argument the other way is of course xkcd#927

[Gabriel Ebner]

Another lemma that would benefit from this type class:

lemma is_basis_empty [subsingleton M] (h_empty : ¬ nonempty ι) : is_basis R (λ x : ι, (0 : M)) :=

[Eric Wieser]

docs#is_basis_empty isn't yet stated exactly like that, but will be soon ;)

[Mario Carneiro]

oh, I spent a while looking at docs#is_basis_empty_bot trying to figure out why it's not a straight generalization of the lemma before it

[Eric Wieser]

Yeah, I have a PR that removes it

[Eric Wieser]

#6281

[Mario Carneiro]

No I mean a generalization in the other direction

[Mario Carneiro]

if you look at the two statements in docgen the only difference is that the _bot lemma has one fewer assumption

[Eric Wieser]

Yes, and it's proved in terms of the other lemma, so I don't understand what you're disagreeing with. Perhaps best to discuss in the PR.

[Yury G. Kudryashov]

We also have some lemmas about supr/infi over an empty type and filters on an empty type.

[Eric Wieser]

My impression is that now we're just waiting for someone to make the PR

[Floris van Doorn]

I've started this on branch#is_empty.

[Yakov Pechersky]

Awesome! (Bikeshedding comment) It's unfortunate that empty is taken, because now is_empty doesn't agree with nonempty