# Zulip Chat Archive

## Stream: general

### Topic: is_empty_elim

#### Johan Commelin (Nov 24 2021 at 09:49):

Can someone explain to me the benefit of

```
/-- Eliminate out of a type that `is_empty` (without using projection notation). -/
@[elab_as_eliminator]
def is_empty_elim [is_empty α] {p : α → Sort*} (a : α) : p a :=
(is_empty.false a).elim
```

over something like

```
/-- Eliminate out of a type that `is_empty` (without using projection notation). -/
@[elab_as_eliminator]
def is_empty_elim' [is_empty α] (a : α) {β : Sort*} : β :=
(is_empty.false a).elim
```

#### Johan Commelin (Nov 24 2021 at 09:50):

It seems to me that `is_empty_elim'`

is much easier to use, also for unification.

#### Gabriel Ebner (Nov 24 2021 at 09:56):

Does anything break if you replace `is_empty_elim`

by the second one?

#### Johan Commelin (Nov 24 2021 at 09:57):

Let me try

#### Johan Commelin (Nov 24 2021 at 10:04):

Aah, there is already

```
/-- Non-dependent version of `is_empty.elim`. Helpful if the elaborator cannot elaborate `h.elim a`
correctly. -/
protected def elim' {β : Sort*} (h : is_empty α) (a : α) : β :=
h.elim a
```

#### Johan Commelin (Nov 24 2021 at 10:05):

I don't really understand why this can't replace the dependent version everywhere. But if I try, then stuff indeed does break.

#### Gabriel Ebner (Nov 24 2021 at 10:09):

This is surprising. Can you post an example of the breakage?

#### Johan Commelin (Nov 24 2021 at 10:27):

Changing to

```
/-- Eliminate out of a type that `is_empty` (without using projection notation). -/
@[elab_as_eliminator]
def is_empty_elim [is_empty α] {p : Sort*} (a : α) : p :=
(is_empty.false a).elim
```

causes the following errors

```
/-
type mismatch at application
iff_true_intro is_empty_elim
term
is_empty_elim
has type
?m_1 → ?m_2 : Sort (imax ? ?)
but is expected to have type
∀ (a : α), p a : Prop
-/
lemma forall_iff {p : α → Prop} : (∀ a, p a) ↔ true :=
iff_true_intro is_empty_elim
---
/-
type mismatch at application
subsingleton.intro is_empty_elim
term
is_empty_elim
has type
?m_1 → ?m_2 : Sort (imax ? ?)
but is expected to have type
∀ (a b : α), a = b : Prop
-/
@[priority 100] -- see Note [lower instance priority]
instance : subsingleton α := ⟨is_empty_elim⟩
```

#### Floris van Doorn (Nov 24 2021 at 10:30):

`is_empty_elim'`

is a special case of `is_empty_elim`

: the latter is only for functions/implications out of an empty type, the former is (also) for dependent functions and universal quantifications over an empty type. Both the errors in the last post are examples of universal quantifications over an empty type.

#### Floris van Doorn (Nov 24 2021 at 10:31):

That said, adding `is_empty_elim'`

to the library seems like a good idea to me.

#### Johan Commelin (Nov 24 2021 at 10:38):

`is_empty.elim'`

is already doing this, as I just discovered.

#### Gabriel Ebner (Nov 24 2021 at 10:43):

I see. IMHO it would also be perfectly reasonable to make `is_empty_elim'`

the default and just write `iff_true_intro (λ a, is_empty_elim a)`

in `forall_iff`

.

Last updated: Dec 20 2023 at 11:08 UTC