Zulip Chat Archive

Stream: general

Topic: if-in-Type

Scott Morrison (Jun 02 2021 at 00:02):

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 (Jun 02 2021 at 00:09):

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 (Jun 02 2021 at 00:17):

@[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 (Jun 02 2021 at 00:20):

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 (Jun 02 2021 at 06:50):

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

Eric Wieser (Jun 02 2021 at 06:51):

Using psum is consistent with docs#classical.type_decidable

Last updated: Aug 03 2023 at 10:10 UTC