18.13. Tuples🔗

The Lean standard library includes a variety of tuple-like types. In practice, they differ in four ways:

whether the first projection is a type or a proposition
whether the second projection is a type or a proposition
whether the second projection's type depends on the first projection's value
whether the type as a whole is a proposition or type

Type	First Projection	Second Projection	Dependent?	Universe
`Prod`	`Type u`	`Type v`	❌️	`Type (max u v)`
`And`	`Prop`	`Prop`	❌️	`Prop`
`Sigma`	`Type u`	`Type v`	✔	`Type (max u v)`
`Subtype`	`Type u`	`Prop`	✔	`Type u`
`Exists`	`Type u`	`Prop`	✔	`Prop`

Some potential rows in this table do not exist in the library:

There is no dependent pair where the first projection is a proposition, because proof irrelevance renders this meaningless.
There is no non-dependent pair that combines a type with a proposition because the situation is rare in practice: grouping data with unrelated proofs is uncommon.

These differences lead to very different use cases. Prod and its variants PProd and MProd simply group data together—they are products. Because its second projection is dependent, Sigma has the character of a sum: for each element of the first projection's type, there may be a different type in the second projection. Subtype selects the values of a type that satisfy a predicate. Even though it syntactically resembles a pair, in practice it is treated as an actual subset. And is a logical connective, and Exists is a quantifier. This chapter documents the tuple-like pairs, namely Prod and Sigma.

18.13.1. Ordered Pairs🔗

The type α × β, which is a notation for Prod α β, contains ordered pairs in which the first item is an α and the second is a β. These pairs are written in parentheses, separated by commas. Larger tuples are represented as nested tuples, so α × β × γ is equivalent to α × (β × γ) and (x, y, z) is equivalent to (x, (y, z)).

syntaxProduct Types

term ::= ...
    | The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.term × term

The product Prod α β is written α × β.

syntaxPairs

term ::= ...
    | Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc. 

Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.(term, term)

structure

Prod.{u, v} (α : Type u) (β : Type v) :
  Type (max u v)

The product type, usually written α × β. Product types are also called pair or tuple types. Elements of this type are pairs in which the first element is an α and the second element is a β.

Products nest to the right, so (x, y, z) : α × β × γ is equivalent to (x, (y, z)) : α × (β × γ).

Conventions for notations in identifiers:

The recommended spelling of × in identifiers is Prod.

Constructor

Prod.mk.{u, v}

Constructs a pair. This is usually written (x, y) instead of Prod.mk x y.

Conventions for notations in identifiers:

The recommended spelling of (a, b) in identifiers is mk.

Fields

fst : α

The first element of a pair.

snd : β

The second element of a pair.

There are also the variants α ×' β (which is notation for PProd α β) and MProd, which differ with respect to universe levels: like PSum, PProd allows either α or β to be a proposition, while MProd requires that both be types at the same universe level. Generally speaking, PProd is primarily used in the implementation of proof automation and the elaborator, as it tends to give rise to universe level unification problems that can't be solved. MProd, on the other hand, can simplify universe level issues in certain advanced use cases.

syntaxProducts of Arbitrary Sorts

term ::= ...
    | A product type in which the types may be propositions, usually written `α ×' β`.

This type is primarily used internally and as an implementation detail of proof automation. It is
rarely useful in hand-written code.


Conventions for notations in identifiers:

 * The recommended spelling of `×'` in identifiers is `PProd`.term ×' term

The product PProd α β, in which both types could be propositions, is written α × β.

structure

PProd.{u, v} (α : Sort u) (β : Sort v) :
  Sort (max (max 1 u) v)

A product type in which the types may be propositions, usually written α ×' β.

This type is primarily used internally and as an implementation detail of proof automation. It is rarely useful in hand-written code.

Conventions for notations in identifiers:

The recommended spelling of ×' in identifiers is PProd.

Constructor

PProd.mk.{u, v}

Fields

fst : α

The first element of a pair.

snd : β

The second element of a pair.

structure

MProd.{u} (α β : Type u) : Type u

A product type in which both α and β are in the same universe.

It is called MProd is because it is the universe-monomorphic product type.

Constructor

MProd.mk.{u}

Fields

fst : α

The first element of a pair.

snd : β

The second element of a pair.

18.13.1.1. API Reference🔗

As a mere pair, the primary API for Prod is provided by pattern matching and by the first and second projections Prod.fst and Prod.snd.

18.13.1.1.1. Transformation

def

Prod.map.{u₁, u₂, v₁, v₂} {α₁ : Type u₁}
  {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
  (f : α₁ → α₂) (g : β₁ → β₂) :
  α₁ × β₁ → α₂ × β₂

Transforms a pair by applying functions to both elements.

Examples:

(1, 2).map (· + 1) (· * 3) = (2, 6)
(1, 2).map toString (· * 3) = ("1", 6)

def

Prod.swap.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} : α × β → β × α

Swaps the elements in a pair.

Examples:

(1, 2).swap = (2, 1)
("orange", -87).swap = (-87, "orange")

18.13.1.1.2. Natural Number Ranges

def

Prod.allI (i : Nat × Nat)
  (f :
    (j : Nat) → i.fst ≤ j → j < i.snd → Bool) :
  Bool

Checks whether a predicate holds for all natural numbers in a range.

In particular, (start, stop).allI f returns true if f is true for all natural numbers from start (inclusive) to stop (exclusive).

Examples:

(5, 8).allI (fun j _ _ => j < 10) = (5 < 10) && (6 < 10) && (7 < 10)
(5, 8).allI (fun j _ _ => j % 2 = 0) = false
(6, 7).allI (fun j _ _ => j % 2 = 0) = true

def

Prod.anyI (i : Nat × Nat)
  (f :
    (j : Nat) → i.fst ≤ j → j < i.snd → Bool) :
  Bool

Checks whether a predicate holds for any natural number in a range.

In particular, (start, stop).allI f returns true if f is true for any natural number from start (inclusive) to stop (exclusive).

Examples:

(5, 8).anyI (fun j _ _ => j == 6) = (5 == 6) || (6 == 6) || (7 == 6)
(5, 8).anyI (fun j _ _ => j % 2 = 0) = true
(6, 6).anyI (fun j _ _ => j % 2 = 0) = false

def

Prod.foldI.{u} {α : Type u} (i : Nat × Nat)
  (f :
    (j : Nat) → i.fst ≤ j → j < i.snd → α → α)
  (init : α) : α

Combines an initial value with each natural number from in a range, in increasing order.

In particular, (start, stop).foldI f init applies fon all the numbers from start (inclusive) to stop (exclusive) in increasing order:

Examples:

(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = (#[] |>.push 5 |>.push 6 |>.push 7)
(5, 8).foldI (fun j _ _ xs => xs.push j) #[] = #[5, 6, 7]
(5, 8).foldI (fun j _ _ xs => toString j :: xs) [] = ["7", "6", "5"]

18.13.1.1.3. Ordering

def

Prod.lexLt.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [LT α] [LT β] (s t : α × β) :
  Prop

Lexicographical order for products.

Two pairs are lexicographically ordered if their first elements are ordered or if their first elements are equal and their second elements are ordered.

18.13.2. Dependent Pairs🔗

Dependent pairs, also known as dependent sums or Σ-types, are pairs in which the second term's type may depend on the value of the first term. They are closely related to the existential quantifier and Subtype. Unlike existentially quantified statements, dependent pairs are in the Type universe and are computationally relevant data. Unlike subtypes, the second term is also computationally relevant data. Like ordinary pairs, dependent pairs may be nested; this nesting is right-associative.

syntaxDependent Pair Types

term ::= ...
    | (`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident : term) × term

term ::= ...
    | Σ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident* (: term)?, term

term ::= ...
    | Σ (`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident* : term), term

Dependent pair types bind one or more variables, which are then in scope in the final term. If there is one variable, then its type is a that of the first element in the pair and the final term is the type of the second element in the pair. If there is more than one variable, the types are nested right-associatively. The identifiers may also be _. With parentheses, multiple bound variables may have different types, while the unparenthesized variant requires that all have the same type.

Nested Dependent Pair Types

The type

Σ n k : Nat, Fin (n * k)

is equivalent to

Σ n : Nat, Σ k : Nat, Fin (n * k)

and

(n : Nat) × (k : Nat) × Fin (n * k)

The type

Σ (n k : Nat) (i : Fin (n * k)) , Fin i.val

is equivalent to

Σ (n : Nat), Σ (k : Nat), Σ (i : Fin (n * k)) , Fin i.val

and

(n : Nat) × (k : Nat) × (i : Fin (n * k)) × Fin i.val

The two styles of annotation cannot be mixed in a single «termΣ_,_» : termΣ-type:

Σ n kunexpected token '('; expected ',' (i : Fin (n * k)) , Fin i.val

<example>:1:5-1:7: unexpected token '('; expected ','

Dependent pairs are typically used in one of two ways:

They can be used to “package” a concrete type index together with a value of the indexed family, used when the index value is not known ahead of time. The type Σ n, Fin n is a pair of a natural number and some other number that's strictly smaller. This is the most common way to use dependent pairs.
The first element can be thought of as a “tag” that's used to select from among different types for the second term. This is similar to the way that selecting a constructor of a sum type determines the types of the constructor's arguments. For example, the type
Σ (b : Bool), if b then Unit else α
is equivalent to Option α, where none is ⟨true, ()⟩ and some x is ⟨false, x⟩. Using dependent pairs this way is uncommon, because it's typically much easier to define a special-purpose inductive type directly.

structure

Sigma.{u, v} {α : Type u} (β : α → Type v) :
  Type (max u v)

Dependent pairs, in which the second element's type depends on the value of the first element. The type Sigma β is typically written Σ a : α, β a or (a : α) × β a.

Although its values are pairs, Sigma is sometimes known as the dependent sum type, since it is the type level version of an indexed summation.

Constructor

Sigma.mk.{u, v}

Constructs a dependent pair.

Using this constructor in a context in which the type is not known usually requires a type ascription to determine β. This is because the desired relationship between the two values can't generally be determined automatically.

Fields

fst : α

The first component of a dependent pair.

snd : β self.fst

The second component of a dependent pair. Its type depends on the first component.

Dependent Pairs with Data

The type Vector, which associates a known length with an array, can be placed in a dependent pair with the length itself. While this is logically equivalent to just using Array, this construction is sometimes necessary to bridge gaps in an API.

def getNLinesRev : (n : Nat) → IO (Vector String n)
  | 0 => pure #v[]
  | n + 1 => do
    let xs ← getNLinesRev n
    return xs.push (← (← IO.getStdin).getLine)

def getNLines (n : Nat) : IO (Vector String n) := do
  return (← getNLinesRev n).reverse

partial def getValues : IO (Σ n, Vector String n) := do
  let stdin ← IO.getStdin

  IO.println "How many lines to read?"
  let howMany ← stdin.getLine

  if let some howMany := howMany.trim.toNat? then
    return ⟨howMany, (← getNLines howMany)⟩
  else
    IO.eprintln "Please enter a number."
    getValues

def main : IO Unit := do
  let values ← getValues
  IO.println s!"Got {values.fst} values. They are:"
  for x in values.snd do
    IO.println x.trim

When calling the program with this standard input:

                      stdin4ApplesQuincePlumsRaspberries

the output is:

                      stdoutHow many lines to read?Got 4 values. They are:RaspberriesPlumsQuinceApples

Dependent Pairs as Sums

Sigma can be used to implement sum types. The Bool in the first projection of Sum' indicates which type the second projection is drawn from.

def Sum' (α : Type) (β : Type) : Type :=
  Σ (b : Bool),
    match b with
    | true => α
    | false => β

The injections pair a tag (a Bool) with a value of the indicated type. Annotating them with match_pattern allows them to be used in patterns as well as in ordinary terms.

variable {α β : Type}

@[match_pattern]
def Sum'.inl (x : α) : Sum' α β := ⟨true, x⟩

@[match_pattern]
def Sum'.inr (x : β) : Sum' α β := ⟨false, x⟩

def Sum'.swap : Sum' α β → Sum' β α
  | .inl x => .inr x
  | .inr y => .inl y

Just as Prod has a variant PProd that accepts propositions as well as types, PSigma allows its projections to be propositions. This has the same drawbacks as PProd: it is much more likely to lead to failures of universe level unification. However, PSigma can be necessary when implementing custom proof automation or in some rare, advanced use cases.

syntaxFully-Polymorphic Dependent Pair Types

term ::= ...
    | Σ' `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident* (: term)? , term

term ::= ...
    | Σ' (`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident* : term), term

The rules for nesting Σ', as well as those that govern its binding structure, are the same as those for «termΣ_,_» : termΣ.

structure

PSigma.{u, v} {α : Sort u} (β : α → Sort v) :
  Sort (max (max 1 u) v)

Fully universe-polymorphic dependent pairs, in which the second element's type depends on the value of the first element and both types are allowed to be propositions. The type PSigma β is typically written Σ' a : α, β a or (a : α) ×' β a.

In practice, this generality leads to universe level constraints that are difficult to solve, so PSigma is rarely used in manually-written code. It is usually only used in automation that constructs pairs of arbitrary types.

To pair a value with a proof that a predicate holds for it, use Subtype. To demonstrate that a value exists that satisfies a predicate, use Exists. A dependent pair with a proposition as its first component is not typically useful due to proof irrelevance: there's no point in depending on a specific proof because all proofs are equal anyway.

Constructor

PSigma.mk.{u, v}

Constructs a fully universe-polymorphic dependent pair.

Fields

fst : α

The first component of a dependent pair.

snd : β self.fst

The second component of a dependent pair. Its type depends on the first component.