choice compatible with products

Stream: general

[Sébastien Gouëzel]

Is there a way to do something like

def my_better_choice (α : Type*) [Nonempty α] : α := by
  match α with
  | X × Y => (my_better_choice X, my_better_choice Y)
  | _ => Classical.choice α

I.e., have a choice function on nonempty types, which is compatible with the projections in product types?

[Sébastien Gouëzel]

I guess no, by the cardinality model (which shows that asking if a type is a product type hasn't a well defined answer).

[Filippo A. E. Nuccio]

Interesting! Can you speculate a bit or point to a reference?

[Kevin Buzzard]

There's a model of Lean where Fin 2 \times Fin 2 and Fin 4 are equal as types.

[Eric Wieser]

Not a great solution, but:

import Mathlib

class HasNiceChoice (α) where
  niceChoice : Nonempty α → α

export HasNiceChoice (niceChoice)

noncomputable instance (priority := low) defaultNiceChoice {α : Type*} : HasNiceChoice α where
  niceChoice := Classical.choice

noncomputable instance Prod.instNiceChoice {α β : Type*}
    [HasNiceChoice α] [HasNiceChoice β] : HasNiceChoice (α × β) where
  niceChoice h := (niceChoice sorry, niceChoice sorry)

[Floris van Doorn]

I expect that it is consistent to assume this, i.e. to assume

axiom prodChoice (α : Type*) [Nonempty α] : α
axiom prodChoice_spec {α β : Type*} [Nonempty α] [Nonempty β] :
  prodChoice (α × β) = (prodChoice α, prodChoice β)

I don't see why this should be inconsistent even in the cardinality model. In the model when defining the interpretation of Prod and Prod.mk I think you can ensure that prodChoice_spec holds.
However, I also expect that such a function is not definable in Lean from ordinary choice.

[Yaël Dillies]

Isn't HasNiceChoice basically docs#Inhabited ?

[Eric Wieser]

Not quite, because HasNiceChoice Empty exists

[Sébastien Gouëzel]

I agree that it's certainly consistent to assume this. However, it is also not provable, because the cardinality model gives you a model where this doesn't hold, as follows.

In the cardinality model, all types with the same cardinality are equal. This can be built by starting from a model where the types are distinct, choosing compatible bijections between the types with the same cardinality, and identifying the types under these bijections. Let me start from such a bijection f between ℕ and ℕ x ℕ. Assume I have distinguished points in each type (say x : ℕ and y : ℕ x ℕ), compatible with the product structure (i.e. y = (x, x)) and with the identifications (i.e. y = f x). Then f x = (x, x). But it is easy to construct f such that this equality is never true (choose for instance f x to not be in the vertical line above x). This shows that, in the cardinality model constructed using this specific f, then prodChoice is false.

[Kyle Miller]

I think this is one of those places where you need your own type universe to keep track of how the type is a product.

import Mathlib.Tactic.Common

universe u

@[pp_with_univ]
inductive PType : Type (u + 1) where
  | incl (α : Type u)
  | prod (α β : PType)

def PType.toType : PType.{u} → Type u
  | .incl α => α
  | .prod α β => α.toType × β.toType

instance : CoeSort PType.{u} (Type u) := ⟨PType.toType⟩

noncomputable def PType.choice (α : PType) [inst : Nonempty α] : α :=
  match α, inst with
  | .incl _, inst => Classical.choice inst
  | .prod α β, inst =>
    have := (nonempty_prod.mp inst).1
    have := (nonempty_prod.mp inst).2
    (PType.choice α, PType.choice β)