14.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.

14.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 ::= ...
    | Product type (aka pair). You can use `α × β` as notation for `Prod α β`.
Given `a : α` and `b : β`, `Prod.mk a b : Prod α β`. You can use `(a, b)`
as notation for `Prod.mk a b`. Moreover, `(a, b, c)` is notation for
`Prod.mk a (Prod.mk b c)`.
Given `p : Prod α β`, `p.1 : α` and `p.2 : β`. They are short for `Prod.fst p`
and `Prod.snd p` respectively. You can also write `p.fst` and `p.snd`.
For more information: [Constructors with Arguments](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html?highlight=Prod#constructors-with-arguments)


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)

Product type (aka pair). You can use α × β as notation for Prod α β. Given a : α and b : β, Prod.mk a b : Prod α β. You can use (a, b) as notation for Prod.mk a b. Moreover, (a, b, c) is notation for Prod.mk a (Prod.mk b c). Given p : Prod α β, p.1 : α and p.2 : β. They are short for Prod.fst p and Prod.snd p respectively. You can also write p.fst and p.snd. For more information: Constructors with Arguments

Conventions for notations in identifiers:

The recommended spelling of × in identifiers is Prod.

Constructor

Prod.mk.{u, v}

Constructs a pair from two terms.

Conventions for notations in identifiers:

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

Fields

fst : α

The first projection out of a pair. if p : α × β then p.1 : α.

snd : β

The second projection out of a pair. if p : α × β then p.2 : β.

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.

syntaxProduct Types

term ::= ...
    | Similar to `Prod`, but `α` and `β` can be propositions.
You can use `α ×' β` as notation for `PProd α β`.
We use this type internally to automatically generate the `brecOn` recursor.


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)

Similar to Prod, but α and β can be propositions. You can use α ×' β as notation for PProd α β. We use this type internally to automatically generate the brecOn recursor.

Conventions for notations in identifiers:

The recommended spelling of ×' in identifiers is PProd.

Constructor

PProd.mk.{u, v}

Fields

fst : α

The first projection out of a pair. if p : PProd α β then p.1 : α.

snd : β

The second projection out of a pair. if p : PProd α β then p.2 : β.

structure

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

Similar to Prod, but α and β are in the same universe. We say MProd is the universe monomorphic product type.

Constructor

MProd.mk.{u}

Fields

fst : α

The first projection out of a pair. if p : MProd α β then p.1 : α.

snd : β

The second projection out of a pair. if p : MProd α β then p.2 : β.

14.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.

14.13.1.1.1. Ordering

def

Prod.lex.{u, v} {α : Type u} {β : Type v}
  (ha : WellFoundedRelation α)
  (hb : WellFoundedRelation β) :
  WellFoundedRelation (α × β)

def

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

Lexicographical order for products

14.13.1.1.2. Transformation

def

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

Prod.map f g : α₁ × β₁ → α₂ × β₂ maps across a pair by applying f to the first component and g to the second.

def

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

Swap the factors of a product. swap (a, b) = (b, a)

14.13.1.1.3. Natural Number Ranges

def

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

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

(5, 8).anyI f = f 5 && f 6 && f 7

def

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

(start, stop).anyI f a returns true if f is true for some natural number from start (inclusive) to stop (exclusive):

(5, 8).anyI f = f 5 || f 6 || f 7

def

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

(start, stop).foldI f a evaluates f on all the numbers from start (inclusive) to stop (exclusive) in increasing order:

(5, 8).foldI f init = init |> f 5 |> f 6 |> f 7

14.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 k expected ','(i : Fin (n * k)) , Fin i.val

<example>:1:6: 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)

Sigma β, also denoted Σ a : α, β a or (a : α) × β a, is the type of dependent pairs whose first component is a : α and whose second component is b : β a (so the type of the second component can depend on the value of the first component). It is sometimes known as the dependent sum type, since it is the type level version of an indexed summation.

Constructor

Sigma.mk.{u, v}

Constructor for a dependent pair. If a : α and b : β a then ⟨a, b⟩ : Sigma β. (This will usually require a type ascription to determine β since it is not determined from a and b alone.)

Fields

fst : α

The first component of a dependent pair. If p : @Sigma α β then p.1 : α.

snd : β self.fst

The second component of a dependent pair. If p : Sigma β then p.2 : β p.1.

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)

PSigma β, also denoted Σ' a : α, β a or (a : α) ×' β a, is the type of dependent pairs whose first component is a : α and whose second component is b : β a (so the type of the second component can depend on the value of the first component). It differs from Σ a : α, β a in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting to Type u and Type v. This means that it can be used in situations where one side is a proposition, like (p : Nat) ×' p = p.

The reason this is not the default is that this type lives in the universe Sort (max 1 u v), which can cause problems for universe level unification, because the equation max 1 u v = ?u + 1 has no solution in level arithmetic. PSigma is usually only used in automation that constructs pairs of arbitrary types.

Constructor

PSigma.mk.{u, v}

Constructor for a dependent pair. If a : α and b : β a then ⟨a, b⟩ : PSigma β. (This will usually require a type ascription to determine β since it is not determined from a and b alone.)

Fields

fst : α

The first component of a dependent pair. If p : @Sigma α β then p.1 : α.

snd : β self.fst

The second component of a dependent pair. If p : Sigma β then p.2 : β p.1.