if-in-Type

Stream: general

[Scott Morrison]

Is it plausible to extend the meaning of if h : X then ... else ... so that X doesn't need to be a Prop, but could be in Type*?

Everything would have exactly the usual meaning: in the "yes" branch, we'd have a term h : X, and in the "no" branch we'd have a term h : X → false.

We'd have to generalize away from decidable_pred, but there's a perfectly sensible notion for arbitrary types, i.e. an algorithm that either produces an element or a proof of X → false. In classical mode this could still apply to every type.

I feel like we could avoid some beating around the bush with nonempty sometimes if if statements were allowed to go for the witness directly.

[Mario Carneiro]

I would prefer for this to be a separate definition, although I don't know if you can declare a notation like if then else yourself in lean 3 - I think that one is implemented directly in C++

[Mario Carneiro]

@[class] inductive {u} choicy (α : Type u) : Type u
| pos : α → choicy
| neg : (α → false) → choicy

noncomputable instance classical.choicy (α) : choicy α :=
by classical; exact
if h : nonempty α then choicy.pos (classical.choice h) else choicy.neg (λ a, h ⟨a⟩)

def type_ite {C} (α : Type*) [d : choicy α] (t : α → C) (e : (α → false) → C) : C :=
choicy.rec_on d t e

I don't really know what kind of types would have nontrivial choicy instances though

[Mario Carneiro]

maybe it would be better to simplify this to eliminate the choicy class and just use this for your choicy ite needs:

noncomputable def choicy_ite {C} (α) (t : α → C) (e : (α → false) → C) : C :=
by classical; exact
if h : nonempty α then t (classical.choice h) else e (λ a, h ⟨a⟩)

[Eric Wieser]

I explored this a little before at https://gist.github.com/eric-wieser/103ad49e8c5c4415991b7622f77c48e0

[Eric Wieser]

Using psum is consistent with docs#classical.type_decidable