• Docència
    • Àlgebra Lineal i Geometria
    • Recull de qüestions
    • Recursos
    • Direcció de treballs
    • Innovació Docent
  • Recerca
    • Publicacions
    • Conferències
  • Codi
    • An Introduction to Lean 4
    • Taller de Lean 4
    • Galeria TikZ
    • Hipotrocoide
    • Evolució espacial dels virus
  • Enllaços
    • Grup d’Investigació
    • Grup d’Innovació Docent
    • Seminari Predoc
    • Congrés Investmat
  1. Empty and Unit types
  • Source Code
  • An Introduction to Lean 4
  • Basic Syntax
  • Propositions
  • Quantifiers
  • Equalities
  • Functions
  • Choice
  • Subtypes
  • Relations
  • Quotients
  • Natural numbers
  • Orders
  • Empty and Unit types
  • Product and Sum types
  • Lists and Monoids

Sections

  • Empty
  • Unit
  • Exercises
    • Empty
    • Unit

Empty and Unit types

Autor

Enric Cosme

Modificat

26/04/2025

In this chapter, we explore two of the simplest—but most fundamental—types in Lean: the Empty type and the Unit type. Though these types may seem trivial at first glance, they play a crucial role in the logic and structure of formal proofs.

Empty

The Empty type, written as Empty, is a type with no inhabitants.

If we #print Empty, Lean returns:

inductive Empty : Type
number of parameters: 0
constructors:

This means that if we have a value of type Empty, we can derive a value of any other type from it. In Lean, this is done using the Empty.elim function, which expresses the logical principle that from falsehood, anything follows.

emptyToAny
def emptyToAny {A : Type} : Empty → A := by
  intro x
  exact Empty.elim x

An interesting property of the emptyToAny function is that it is unique up to definitional equality; any two functions with type Empty → A are definitionally the same.

emptyToAny
theorem emptyToAnyUnique {A : Type} {f g : Empty → A} : f = g := by
  funext x
  exact Empty.elim x

This implies that the emptyToAny function with codomain Empty is, in particular, the identity function on Empty.

emptyToAny
theorem emptyToAnyId : @emptyToAny Empty = id := by
  funext x
  exact Empty.elim x

Unit

The Unit type, written as Unit, is a type with exactly one inhabitant: Unit.unit, usually just written ().

If we #print Unit, Lean returns:

@[reducible] def Unit : Type :=
PUnit

There is always a function from any type to the Unit type, since we can simply ignore the input and return ().

anyToUnit
def anyToUnit {A : Type} : A → Unit := by
  intro _
  exact ()

The anyToUnit function is unique up to definitional equality; any two functions with type A → Unit are definitionally the same.

anyToUnit
theorem anyToUnitUnique {A : Type} {f g : A → Unit} : f = g := by
  funext x
  exact rfl

This implies that when the domain is Unit, the anyToUnit function is, in particular, the identity function on Unit.

anyToUnit
theorem anyToUnitId : @anyToUnit Unit = id := by
  funext x
  exact rfl

Exercises

Empty

Exercises.lean
-- All the elements of `Empty` are equal
theorem emptyUnique : ∀ (x y : Empty), x = y := by sorry

-- The `emptyToAny` function is injective
theorem emptyToAnyInj {A : Type} : injective (@emptyToAny A) := by sorry

-- Under `Classical.choice`, if the `emptyToAny` function is surjective, the codomain cannot be `Nonempty`
theorem emptyToAnySurj {A : Type} : surjective (@emptyToAny A) ↔ ¬ (Nonempty A) := by sorry

Unit

Exercises.lean
-- All the elements of `Unit` are equal
theorem unitUnique : ∀ (x y : Unit), x = y := by sorry

-- The `anyToUnit` function is injective if, and only if, the domain has only one element
theorem anyToUnitInj {A : Type} : injective (@anyToUnit A) ↔ (∀ (a1 a2 : A), a1 = a2) := by sorry
  
-- Under `Classical.choice`, the `anyToUnit` function is surjective if and only if the domain is `Nonempty`
theorem anyToUnitSurj {A : Type} : surjective (@anyToUnit A) ↔ Nonempty A := by sorry

2025 Enric Cosme Llópez

Dr. Moliner, 50 | 46100, Burjassot, València

Dissenyat amb & Quarto