is_empty_elim

Stream: general

[Johan Commelin]

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]

It seems to me that is_empty_elim' is much easier to use, also for unification.

[Gabriel Ebner]

Does anything break if you replace is_empty_elim by the second one?

[Johan Commelin]

Let me try

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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]

That said, adding is_empty_elim' to the library seems like a good idea to me.

[Johan Commelin]

is_empty.elim' is already doing this, as I just discovered.

[Gabriel Ebner]

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.