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

Subtype p, usually written as {x : α // p x}, is a type which represents all the elements x : α for which p x is true. It is structurally a pair-like type, so if you have x : α and h : p x then ⟨x, h⟩ : {x // p x}. An element s : {x // p x} will coerce to α but you can also make it explicit using s.1 or s.val.

Conventions for notations in identifiers:

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

Constructor

Subtype.mk.{u}

Fields

val : α

If s : {x // p x} then s.val : α is the underlying element in the base type. You can also write this as s.1, or simply as s when the type is known from context.

property : p self.val

If s : {x // p x} then s.2 or s.property is the assertion that p s.1, that is, that s is in fact an element for which p holds.

syntaxSubtypes
term ::= ...
    | `Subtype p`, usually written as `{x : α // p x}`, is a type which
represents all the elements `x : α` for which `p x` is true. It is structurally
a pair-like type, so if you have `x : α` and `h : p x` then
`⟨x, h⟩ : {x // p x}`. An element `s : {x // p x}` will coerce to `α` but
you can also make it explicit using `s.1` or `s.val`.


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 ::= ...
    | `Subtype p`, usually written as `{x : α // p x}`, is a type which
represents all the elements `x : α` for which `p x` is true. It is structurally
a pair-like type, so if you have `x : α` and `h : p x` then
`⟨x, h⟩ : {x // p x}`. An element `s : {x // p x}` will coerce to `α` but
you can also make it explicit using `s.1` or `s.val`.


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