Help: recursor 'Exists.casesOn' can only eliminate into Prop

Stream: lean4

[Snir Broshi]

Let's say I have the following definition:

def f : False := by
  have h : ∃ x : ℕ, True := ⟨0, trivial⟩
  have ⟨y, h'⟩ := h
  sorry

So far so good. I'm defining some random stuff with have.
If I change the False to ℕ (or to any other Type):

def f : ℕ := by
  have h : ∃ x : ℕ, True := ⟨0, trivial⟩
  have ⟨y, h'⟩ := h
  sorry

it gives the following error:

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop
motive : (∃ x, True) → Sort ?u.4525
h_1 : (y : ℕ) → (h' : True) → motive ⋯
h✝ : ∃ x, True
⊢ 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

I don't understand how the return type of the function has anything to do with the unrelated have definitions inside it. Why can I only destruct an existential statement when the goal is a Type?
Thanks!

[Kyle Miller]

Here's some discussion from two days ago: #new members > ✔ Why can't I "unwrap" exists inside a : Prop function? @ 💬

[Kenny Lau]

@Snir basically because of proof irrelevance (any two proofs of a proposition are equal), there is no way to construct an algorithm to give you back the witness of an exists proof

[Kenny Lau]

you'll have to use choose in some form

[Kenny Lau]

import Mathlib.Tactic

noncomputable def f : ℕ := by
  have h : ∃ x : ℕ, True := ⟨0, trivial⟩
  choose y h' using h
  exact y

noncomputable def f' : ℕ :=
  have h : ∃ x : ℕ, True := ⟨0, trivial⟩
  h.choose

def f'' : ℕ :=
  have h : ∃ x : ℕ, True := ⟨0, trivial⟩
  Nat.find h

[Kenny Lau]

here are the workarounds, and please note that you shouldn't use by in definitions

[Snir Broshi]

Huh, so the only issue is I should use the choose syntax instead of angle brackets? Also, why does proof-irrelevance force using the axiom of choice here? I'm not asking for a particular witness, just for one that was constructed in the proof of h, so the proof of 2 = 4 in the linked thread baffles me (and also doesn't type-check even if I replace the bad destructuring of the existential statement with sorry).
Also, why does this fail:

noncomputable def f''' (h : ∃ x : ℕ, True) := by
  choose y h' using h
  exact y

(I moved h to the hypothesis, and let the return type be inferred instead of explicit)

[Kyle Miller]

The problem is that there are often multiple witnesses that work for the same existential. When you see have ⟨y, h'⟩ := h, you should think "we will reduce h to be of the form Exists.mk y h' and then use the computed values for y and h'.

The problem is that if you have two different proofs of the existential, these proofs are equal, and you can use that to prove that the witnesses are equal, even if they're different. That's a contradiction.

[Snir Broshi]

I don't see how you would prove that, since all we get is a witness which we know nothing about.
Sure there can be multiple witnesses, but since we know a constructive proof exists, I can copy-paste the proof of it inside my own theorem, so why wouldn't Lean allow me to get a constructive witness which we know exists?
Let's say I try to prove 1 = 2:

def f : ℕ := by
  have h1 : ∃ x, True := ⟨1, trivial⟩
  have h2 : ∃ x, True := ⟨2, trivial⟩
  have ⟨a1, t1⟩ := h1
  have ⟨a2, t2⟩ := h2
  have h : h1 = h2 := rfl
  have h1' : h1 = ⟨a1, t1⟩ := rfl
  have h2' : h1 = ⟨a2, t1⟩ := rfl
  have p : 1 = 2 := sorry

I don't see how to prove a1 = a2 from anything here, not to mention a1 = 1 and a2 = 2. Is there a way?

[Matt Diamond]

you should think of Prop as being an opaque thing that you can't computably extract data from (with exceptions)

there's often a non-Prop data-carrying structure that you can use instead... for example, the data version of Exists would be Subtype

[Matt Diamond]

so instead of ∃ x, True you would define a value of type { n : ℕ // True }

[Matt Diamond]

then you won't have any problems extracting the value

[Kyle Miller]

@Snir Maybe this helps?

The idea is that if you could extract a witness in a non-Prop context, then you could actually define a projection function, and then by substituting h1 = h2 you can show that two different witnesses are equal.

[Snir Broshi]

Woah. So when would people use Exists rather than Subtype? Only when using the axiom of choice?
And if Lean defined an axiom of choice for Subtype, would it be inconsistent?
How does one prove 1 = 2 in the example above?

[Kenny Lau]

@Snir people use Prop because they want to state propositions, that's about it

[Kenny Lau]

if you don't want proof irrelevance etc., you would be doing homotopy type theory (HoTT)

[Kenny Lau]

if you don't want proof irrelevance, subtypes would get a bit messy, because if I have two different proofs of e < pi, then I would have two different elements of { x : R | x < pi }, both of which project to e.

[Snir Broshi]

@Kyle Miller To me it looks like the problem is the second axiom you defined.
What if instead we have:

axiom Exists.extract {α : Sort _} {p : α → Prop} : (∃ x, p x) → α

axiom Exists.extract_mk' {α : Sort _} {p : α → Prop} {x : α} (h : p x) :
    p (Exists.extract (Exists.intro x h))

Can you now prove False? Maybe the problem is that the angle brackets syntax uses casesOn which you said is problematic somehow, and what I want is this Exists.extract_mk'?

[Kenny Lau]

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

theorem foo {x y : { z : ℝ // z < Real.pi }}
    (hx : x.1 = Real.exp 1) (hy : y.1 = Real.exp 1) : x = y :=
  Subtype.ext <| hx.trans hy.symm

[Kenny Lau]

@Snir then that is alright, except that you can't demand that it picks out the witness you choose

[Kenny Lau]

the two axioms you stated are consistent with mathlib's foundation, more specifically, what you stated are just Exists.choose and Exists.choose_spec

[Kenny Lau]

@Snir

noncomputable def Exists.extract {α : Sort _} {p : α → Prop} : (∃ x, p x) → α :=
  Exists.choose

theorem Exists.extract_mk' {α : Sort _} {p : α → Prop} {x : α} (h : p x) :
    p (Exists.extract (Exists.intro x h)) :=
  Exists.choose_spec ⟨x, h⟩

[Kyle Miller]

@Snir Read the second post too, where it shows how to define extract using the "bad" casesOn that would permit angle bracket notation in a non-Prop context.

[Kyle Miller]

There's nothing wrong with Exists.extract on its own, but the problem is that Exists.extract_mk is a consequence of being able to do angle bracket notation in a non-Prop context, and that's what leads to a contradiction.

Using Exists.choose (Classical.choice) is the workaround, since it picks out some witness, rather than the witness encoded inside the proof term.

[Matt Diamond]

here's a proof that you can't get the value out of Exists:

import Mathlib

axiom bad {α : Type*} {p : α → Prop} {a : α} (ha : p a)
  : Exists.choose (⟨a, ha⟩ : ∃ a, p a) = a

example : False :=
by
  let a : ∃ (b : Bool), True := ⟨true, trivial⟩
  let b : ∃ (b : Bool), True := ⟨false, trivial⟩
  have a_eq_b : a = b := rfl
  have ha : a.choose = true := bad trivial
  have hb : b.choose = false := bad trivial
  rw [a_eq_b, hb] at ha
  contradiction

[Snir Broshi]

@Kenny Lau Exists.choose is noncomputable, but shouldn't there be a computable way to get a witness, as long as the first argument for Exists.intro in the proof for that Exists was computable?

[Kenny Lau]

@Snir see my third workaround

[Snir Broshi]

@Kyle Miller Why is Exists.casesOn'_intro required for the angle brackets? Can't I have just Exists.casesOn'? Then you can't prove False

[Snir Broshi]

@Kenny Lau I can't find what you're referencing, only your noncomputable Exists.choose

[Kyle Miller]

That's the computation rule for it. Without that axiom, you can't prove that Exists.casesOn' actually extracts the witness. It could just use Exists.choose for example, which gives some arbitrary witness.

[Snir Broshi]

But I can use motive w h := (w, h) and then h is of type p w, so I got an arbitrary witness with a proof that it satisfies the property. I don't see why Exists.casesOn'_intro is required for that

[Kenny Lau]

Kenny Lau said:

import Mathlib.Tactic

noncomputable def f : ℕ := by
  have h : ∃ x : ℕ, True := ⟨0, trivial⟩
  choose y h' using h
  exact y

noncomputable def f' : ℕ :=
  have h : ∃ x : ℕ, True := ⟨0, trivial⟩
  h.choose

def f'' : ℕ :=
  have h : ∃ x : ℕ, True := ⟨0, trivial⟩
  Nat.find h

@Snir the last one here

[Aaron Liu]

Snir said:

But I can use motive w h := (w, h) and then h is of type p w, so I got an arbitrary witness with a proof that it satisfies the property. I don't see why Exists.casesOn'_intro is required for that

Is (w, h) of type Prop? The motive has to be a prop.

[Kyle Miller]

(That third one @Kenny Lau is giving the least witness though, which might not be the original witness, and might take a lot of time to find.)

[Kenny Lau]

what on earth is Exists.casesOn'_intro?

[Kyle Miller]

@Kenny Lau:
Kyle Miller said:

Snir Maybe this helps?

[Snir Broshi]

@Aaron Liu no, but we're discussing a variant of Exists.casesOn which accepts Sort, and I asked whether it exists and whether it's consistent

[Aaron Liu]

@Snir but (w, h) isn't even a type, you have to return a type, you can be returning something of type (w, h), did you mean the minor premise and not the motive?

[Snir Broshi]

@Kenny Lau Cool, but that only works for Nat, right? Sounds like I have to use Subtype if I want an existential statement plus remember that it's a constructive proof so that I can choose a witness without the axiom of choice

[Snir Broshi]

Thanks for the help guys, final thoughts:
Based on the threads @Kyle Miller links, and this thread itself, it looks like this is a pretty common pitfall for beginners. I read the pitfalls docs, including the part about proof-irrelevance), including "Trying to extract data from proofs of propositions", but evidently I mostly skimmed it.
Can we maybe add an Exists example to it, and specifically include the error message recursor 'Exists.casesOn' can only eliminate into Prop so beginners can find it?
Perhaps even edit the error message in Lean to add a link to that document?

[Aaron Liu]

If you use the cases tactic directly I think you get a better error message but for obtain it's this one which can be difficult to figure out if you don't already know what it means

[Snir Broshi]

Kenny Lau said:

please note that you shouldn't use by in definitions

Can you explain why not? I can't use tactics like choice without by

[Kyle Miller]

There was a parallel discussion today about exists elimination today that you might be interested in @Snir: #new members > Why is choice more powerful than exists hypothesis? @ 💬

There was also something about ExistsUnique yesterday: #new members > get the witness of `∃!`? @ 💬

[Kyle Miller]

Regarding by and definitions, it's "shouldn't" rather than "mustn't". When you use tactics, you lose control of what the actual definitions are, and so it becomes more difficult to reason about the definitions. If that doesn't matter to you, and you don't care about whether the definition is computable, there's no problem, but this is very infrequent in my experience.

You mentioned "what if you have computable witnesses" before: in that case, the usual recommendation is to make a separate definition for that witness and prove that this definition satisfies a given property.