The Lean Language Reference

18.17. Subtypes🔗

The structure Subtype represents the elements of a type that satisfy some predicate. They are used pervasively both in mathematics and in programming; in mathematics, they are used similarly to subsets, while in programming, they allow information that is known about a value to be represented in a way that is visible to Lean's logic.

Syntactically, an element of a Subtype resembles a tuple of the base type's element and the proof that it satisfies the proposition. They differ from dependent pair types (Sigma) in that the second element is a proof of a proposition rather than data, and from existential quantification in that the entire Subtype is a type rather than a proposition. Even though they are pairs syntactically, Subtype should really be thought of as elements of the base type with associated proof obligations.

Subtypes are trivial wrappers. They are thus represented identically to the base type in compiled code.

🔗structure
Subtype.{u} {α : Sort u} (p : α → Prop) :
  Sort (max 1 u)

All the elements of a type that satisfy a predicate.

Subtype p, usually written { x : α // p x } or { x // p x }, contains all elements x : α for which p x is true. Its constructor is a pair of the value and the proof that it satisfies the predicate. In run-time code, { x : α // p x } is represented identically to α.

There is a coercion from { x : α // p x } to α, so elements of a subtype may be used where the underlying type is expected.

Examples:

  • { n : Nat // n % 2 = 0 } is the type of even numbers.

  • { xs : Array String // xs.size = 5 } is the type of arrays with five Strings.

  • Given xs : List α, List { x : α // x ∈ xs } is the type of lists in which all elements are contained in xs.

Conventions for notations in identifiers:

  • The recommended spelling of { x // p x } in identifiers is subtype.

Constructor

Subtype.mk.{u}

Fields

val : α

The value in the underlying type that satisfies the predicate.

property : p self.val

The proof that val satisfies the predicate p.

syntaxSubtypes
term ::= ...
    | All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.{ ident : term // term }

{ x : α // p } is a notation for Subtype fun (x : α) => p.

The type ascription may be omitted:

term ::= ...
    | All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.{ ident // term }

{ x // p } is a notation for Subtype fun (x : _) => p.

Due to proof irrelevance and η-equality, two elements of a subtype are definitionally equal when the elements of the base type are definitionally equal. In a proof, the ext tactic can be used to transform a goal of equality of elements of a subtype into equality of their values.

Definitional Equality of Subtypes

The non-empty strings s1 and s2 are definitionally equal despite the fact that their embedded proof terms are different. No case splitting is needed in order to prove that they are equal.

def NonEmptyString := { x : String // x ≠ "" } def s1 : NonEmptyString := ⟨"equal", ne_of_beq_false rfl⟩ def s2 : NonEmptyString where val := "equal" property := fun h => List.cons_ne_nil _ _ (String.data_eq_of_eq h) theorem s1_eq_s2 : s1 = s2 := ⊢ s1 = s2 All goals completed! 🐙
Extensional Equality of Subtypes

The non-empty strings s1 and s2 are definitionally equal. Ignoring that fact, the equality of the embedded strings can be used to prove that they are equal. The ext tactic transforms a goal that consists of equality of non-empty strings into a goal that consists of equality of the strings.

abbrev NonEmptyString := { x : String // x ≠ "" } def s1 : NonEmptyString := ⟨"equal", ne_of_beq_false rfl⟩ def s2 : NonEmptyString where val := "equal" property := fun h => List.cons_ne_nil _ _ (String.data_eq_of_eq h) theorem s1_eq_s2 : s1 = s2 := ⊢ s1 = s2 ⊢ s1.val = s2.val All goals completed! 🐙

There is a coercion from a subtype to its base type. This allows subtypes to be used in positions where the base type is expected, essentially erasing the proof that the value satisfies the predicate.

Subtype Coercions

Elements of subtypes can be coerced to their base type. Here, nine is coerced from a subtype of Nat that contains multiples of 3 to Nat.

abbrev DivBy3 := { x : Nat // x % 3 = 0 } def nine : DivBy3 := ⟨9, ⊢ 9 % 3 = 0 All goals completed! 🐙⟩ set_option eval.type true in 10 : Nat#eval Nat.succ nine 
10 : Nat