Choice

Reasoning about types often requires distinguishing between those that are merely nonempty and those that are inhabited. While both concepts assert the existence of elements in a type, they differ in logical strength and computational implications. A type is nonempty if it contains at least one element, but this existence is not necessarily constructive—it does not provide an explicit example. In contrast, a type is inhabited if we can specify a concrete default element, making it more useful in computational contexts. This distinction becomes particularly significant when comparing constructive and classical reasoning. In constructive logic, knowing that a type is nonempty does not guarantee that we can extract an element from it, whereas in classical logic, the axiom Classical.choice allows us to select an element from a nonempty type, thereby making it inhabited.

In this chapter, we will explore the definitions of Inhabited and Nonempty, examine their properties, and analyze their relationship. We will also discuss the role of Classical.choice in bridging the gap between nonemptiness and inhabitation, along with the implications of relying on nonconstructive principles in formal proofs.

Inhabited types

The Inhabited α typeclass ensures that the type α has a designated element, known as default : α. This property is sometimes referred to as making α a “pointed type.”

If we #print Inhabited, Lean returns:

class Inhabited.{u} : Sort u → Sort (max 1 u)
number of parameters: 1
constructor:
Inhabited.mk : {α : Sort u} → α → Inhabited α
fields:
default : α

A typeclass is a special kind of structure that defines a set of properties or operations that a type can possess. We will explore typeclasses further in later chapters. The definition above shows that Inhabited is a typeclass with a single parameter, α, and a constructor, Inhabited.mk, which takes an element of α and produces an instance of Inhabited α. The default field provides access to this designated element.

To define a specific instance of a type class, we use the instance or def keywords. For the Inhabited typeclass, we only need to specify a default element. In the example below, we declare an instance of Inhabited Bool where the default value is true.

InBool.lean

instance InBool : Inhabited Bool := { default := true }

#check InBool -- returns InBool : Inhabited Bool
#print InBool -- returns def InBool : Inhabited Bool := { default := true }
#eval InBool.default -- returns true

Lean provides predefined instances of the Inhabited type class for several types. These instances specify a default value for each type.

instInhabited.lean

#print instInhabitedBool -- default := false 
#print instInhabitedProp -- default := True
#print instInhabitedNat  -- default := Nat.zero

In these cases, Bool has false as its default value, Prop has True, and Nat has 0. These defaults ensure that each type has at least one canonical element available.

Nonempty

The Nonempty type is an inductive proposition that asserts the existence of at least one element in a given type.

If we #print Nonempty, Lean returns

inductive Nonempty.{u} : Sort u → Prop
number of parameters: 1
constructors:
Nonempty.intro : ∀ {α : Sort u}, α → Nonempty α

This means that Nonempty is an inductive type that requires a type α : Sort u as a parameter. The only constructor of Nonempty is Nonempty.intro. This states that for any type α, if we have an element a : α, then we can construct a proof of Nonempty α. In other words, Nonempty α is true if there exists at least one instance of α. Note that Nonempty α asserts that α has at least one element but does not specify this element. Unlike Inhabited α, which requires an explicit default value, Nonempty α only requires an existence proof.

For example, we can prove that Bool is nonempty by constructing a Nonempty Bool instance using the intro constructor.

Nonempty Bool.lean

theorem TNEBool : Nonempty Bool := Nonempty.intro true

This proof shows that Bool is nonempty by providing true as a witness. Since Nonempty α only requires the existence of at least one element in α, choosing true suffices to establish the proof.

Inhabited implies Nonempty

We have a straightforward implication: if a type is inhabited, then it is also nonempty. The following code defines a function that converts an Inhabited A instance into a Nonempty A proof.

Inhabited To Nonempty.lean

def InhabitedToNonempty {A : Type} : Inhabited A → Nonempty A := by
  intro h
  exact Nonempty.intro h.default

Choice

The reverse implication, Nonempty A → Inhabited A, does not always hold in constructive logic. A proof of Nonempty A only asserts the existence of an element without providing a specific one, whereas Inhabited A requires a concrete, predefined default value. In classical logic, we can recover Inhabited A from Nonempty A using the axiom of choice (Classical.choice), but this is noncomputable, meaning we cannot explicitly construct the default element. Consequently, while nonemptiness implies the mere existence of an element, inhabitation requires an explicit and fixed representative, making the two concepts distinct in constructive mathematics.

If we #print Classical.choice, Lean returns

axiom Classical.choice.{u} : {α : Sort u} → Nonempty α → α

This states that for any type α : Sort u, if α is nonempty, then we can obtain an actual element of α. Note that Classical.choice is an axiom. Many axioms, such as Classical.choice, are nonconstructive in nature, meaning they assert the existence of certain objects without providing explicit constructions. As a result, these axioms are often noncomputable and cannot be used in computational contexts.

Nonempty implies Inhabited in Classical Logic

Consider the following function.

Nonempty To Inhabited.lean

noncomputable def NonemptyToInhabited {A : Type} : Nonempty A → Inhabited A := by
  intro h
  have a : A := Classical.choice h
  exact Inhabited.mk a

The function NonemptyToInhabited demonstrates how a proof of nonemptiness can be converted into a proof of inhabitation. Given that Nonempty A asserts the existence of at least one element in the type A, the function uses Classical.choice to extract a : A, a specific element of type A from the existence proof h. The extracted element is then used to construct a proof of inhabitation using Inhabited.mk, which asserts that A has a predefined default element. This function is marked as noncomputable because the choice of an element is nonconstructive: while the existence of an element is guaranteed, the method of selecting it cannot be explicitly computed.

Choose

The command Classical.choose is a function from classical logic that enables the selection of an element satisfying a given predicate. Specifically, given the existence of an element x : X such that a proposition P x holds (i.e., ∃ x : X, P x), Classical.choose returns one such element x for which P x is true. Classical.choose is a direct consequence of Classical.choice; in fact, the two concepts are interderivable. Additionally, the command Classical.choose_spec guarantees that the element extracted indeed satisfies the predicate, providing a formal guarantee that the selected element meets the required condition.

In most situations, we can also use the alternative commands Exists.choose and Exists.choose_spec instead of Classical.choose and Classical.choose_spec. Here is an example of how it is used.

Nonempty To Inhabited.lean

theorem TCarNonempty {A : Type} : Nonempty A ↔ ∃ (a : A), a = a := by 
  apply Iff.intro 
  -- Nonempty A → ∃ a, a = a
  intro h 
  apply Exists.intro (Classical.choice h) 
  exact rfl 
  -- (∃ a, a = a) → Nonempty A
  intro h 
  have a : A := Exists.choose h 
  exact Nonempty.intro a 

Exercises

Under Classical.Choice, any injective function with a nonempty domain admits a left inverse.

Exercises.lean

-- Under `Classical.Choice`, if a function is injective and the domain is 
-- `Nonempty` then the function has a left inverse
theorem TInjtoHasLeftInv {A B : Type} {f : A → B} : injective f → 
Nonempty A → hasleftinv f := by sorry

Under Classical.Choice, every surjective function admits a right inverse. Furthermore, if the function is bijective, this inverse also serves as a left inverse. Thus, assuming Classical.Choice, bijectivity is equivalent to being an isomorphism.

Exercises.lean

-- Under `Classical.Choice`, every surjective function has a right inverse
noncomputable def Inverse {A B : Type} (f : A → B) (h : surjective f) : B → A := by
  intro b
  specialize @h b
  exact Exists.choose h
  
-- Under `Classical.Choice`, the inverse of a surjective function is a right inverse
theorem InvR {A B : Type} (f : A → B) (h : surjective f) :  
f ∘ (Inverse f h)  = id := by sorry

-- Under `Classical.Choice`, every surjective function has a right inverse
theorem TSurjtoHasRightInv {A B : Type} {f : A → B} : surjective f 
→ hasrightinv f := by sorry

-- Under `Classical.Choice`, the inverse of a bijective function is a left inverse
theorem InvL {A B : Type} (f : A → B) (h : bijective f) : 
(Inverse f h.right) ∘ f = id := by sorry

-- Under `Classical.Choice` bijective and isomorphism are equivalent concepts
theorem TCarBijIso {A B : Type} {f : A → B} : bijective f ↔ isomorphism f := 
by sorry