Got "tactic 'induction' failed, recursor 'Exists.casesOn'"

Stream: new members

[James]

Hi all, I thought I can directly prove axiom of choice within lean's type system (which is obviously not the case). Here was my attempt. Given the condition h: ∃ (y : β x), r x y) I was trying to define a function f and use let ⟨y, rxy⟩ := h inside the function to get an instance of y. But then I got the following error :

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop

I guess there is some restriction that prevent me from destructing ∃ inside a plain function (which is kind of surprising to me because I thought every theorem is also a function).

My question: What exactly is this restriction that prevented me from doing so? Is it completely done with Lean's type system? Or is it some additional rule?

[Ruben Van de Velde]

You need to use docs#Exists.choose which is exactly AC in this case again

[Yakov Pechersky]

The concept that prevents you from extracting from a Prop to a Type of related to that's known as "large elimination"

[Giacomo Stevanato]

When you try to destructure a value you're actually using a recursor on it. In this case that's Exists.casesOn which has the following signature:

Exists.casesOn.{u} {α : Sort u} {p : α → Prop} {motive : Exists p → Prop} (t : Exists p)
  (intro : ∀ (w : α) (h : p w), motive ⋯) : motive t

Notice how its motive has type Exists p → Prop.

The way the desugaring is done makes it so that motive must be chosen so that the value you ultimately want to produce will have type motive h (where h was your h: ∃ (y : β x), r x y)). But motive h must live in Prop, so effectively you can only destructure ∃ in a scope that produces a value of a type that is Prop. This has nothing to do with whether you are in a "normal function" or a theorem, though a theorem does additionally force you to produce a value of a type that is Prop anyway.