nonempty_iff_false

Stream: general

[Johan Commelin]

Should we add the following simp lemmas? Or are they bad for some reason?

@[simp] lemma nonempty_iff_false {X : Type*} [h : is_empty X] : nonempty X ↔ false :=
by simp only [not_nonempty_iff.mpr h]

@[simp] lemma is_empty_iff_false {X : Type*} [h : nonempty X] : is_empty X ↔ false :=
by simp only [← not_nonempty_iff, not_true, h]

[Gabriel Ebner]

We already have docs#not_is_empty_of_nonempty (which replaces is_empty_iff_false), and it's a simp lemma. We could also add the following:

@[simp] lemma nonempty_iff_true [nonempty X] : nonempty X ↔ true := ...
@[simp] lemma is_empty_iff_true [is_empty X] : is_empty X ↔ true := ...

[Eric Wieser]

Can [is_empty X] [nonempty X] : false work as a simp lemma?

[Eric Wieser]

The one you link doesn't take both as typeclass arguments

[Gabriel Ebner]

I believe that will work, but I don't think it's useful. It will rewrite false to true (when both instances are available).

[Johan Commelin]

My use case is the following:

casesI is_empty_or_nonempty X,
{ simp }, -- please rewrite all occurences of `nonempty X` to `false`
{ simp }, -- please rewrite all occurences of `is_empty X` to `false`

[Gabriel Ebner]

The second one should already work.

[Yury G. Kudryashov]

BTW, I think that inhabit should do something similar to nontriviality, i.e. try to solve the is_empty case using a specialized simp set

[Yury G. Kudryashov]

This set should include lemmas like tendsto_of_is_empty

[Johan Commelin]

Also, I would like to be able to write inhabit X with x.