Help with unpacking existentials

Stream: new members

[Ben Selfridge]

Hello! Can anyone help me understand why, in the first two examples, I get an error when trying to unpack h, but not in the third example? Thanks!

def even (x : Nat) := ∃ y, x = y + y

structure Even where
  x : Nat
  y : Nat
  hx : x = y + y

example {x} (h : even x) : Even := Even.mk
  (by have ⟨_, _⟩ := h; sorry)
  (by sorry)
  (by sorry)

example {x} (h : even x) : Even := Even.mk 4
  (by have ⟨_, _⟩ := h; sorry)
  (by sorry)

example {x} (h : even x) : Even := by
  apply Even.mk 4
  . have ⟨y, hy⟩ := h; sorry
  . sorry

I'm getting the following error in the first two examples:

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop
x : Nat
motive : even x → Sort ?u.654
h_1 : (w : Nat) → (h : x = w + w) → motive ⋯
h✝ : even x
⊢ motive h✝
 after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

[Etienne Marion]

You can only destruct an exists statement with have (or obtain or rcases that's the same) if what you want to get is a proof of something, i.e. your output type needs to have type Prop. That's what is meant by "can only eliminate into Prop". The reason is that the statement there exists ... does not contain any data, only a property, and you can't produce data out of nothing, you need the axiom of choice to do that. This is explained for example here.

In your first example, the output type is Nat which has type Type so it's data, it does not work. Same for the second example. In the third example however, you have to prove 4 = ?y + ?y, which has type Prop, so you are allowed to do it.

[Aaron Liu]

Existentials can only be unpacked inside of a proof.

[Matt Diamond]

You do have the option to use docs#Exists.choose if you want to get what's inside an existential, as long as you're okay with sacrificing computability

[Matt Diamond]

def even (x : Nat) := ∃ y, x = y + y

structure Even where
  x : Nat
  y : Nat
  hx : x = y + y

noncomputable
example {x} (h : even x) : Even := Even.mk x h.choose h.choose_spec

[Eric Wieser]

Though in that particular example it's silly to do so, you can use / 2 instead

[Matt Diamond]

fair point

[Ben Selfridge]

I think I get it. It's the difference between saying "There exists a number with property P" and "54 has property p". The second thing requires strictly more information, so if you are promising you're going to provide an actual number as part of your output type, an existential just can never give you what you need.