## 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?

Let me try

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

/-- 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: Aug 03 2023 at 10:10 UTC