Subtypes

This chapter explores the definition and usage of subtypes in Lean. We will introduce their basic properties, discuss common operations, and demonstrate their application in mathematical reasoning and program verification.

A subtype is a way to define a restricted entity of a given type by specifying a condition that the elements of this type must satisfy. A subtype of a type A is typically defined using a predicate P : A → Prop, which assigns a proposition to each element of A. The corresponding subtype, denoted as Subtype P or {a : A // P a}, consists of all elements a : A that satisfy P.

Subtype.lean

-- We define variables A : Type and P : A → Prop, a predicate on A
variable (A : Type)
variable (P : A → Prop)
-- With this information we can obtain `Subtype P`
#check Subtype P
-- An alternative notation is
#check { a : A // P a }

Subtypes play a crucial role in formal verification, as they allow us to encode mathematical objects with additional properties. For example, we can define the subtype of even natural numbers, the positive real numbers, or the set of invertible matrices. By doing so, we ensure that any element of the subtype inherently satisfies the given condition, reducing the need for repetitive proof obligations.

If we #print Subtype, Lean returns

structure Subtype.{u} : {α : Sort u} → (α → Prop) → Sort (max 1 u)
number of parameters: 2
constructor:
Subtype.mk : {α : Sort u} → {p : α → Prop} → (val : α) → p val → Subtype p
fields:
val : α
property : p self.val

The Subtype structure in Lean is parameterized by a type α and a predicate p : α → Prop, which defines adscription to the subtype. It includes a constructor, Subtype.mk, that takes a value val : α along with a proof of p val, ensuring that val satisfies the predicate. An instance of Subtype p has two fields: val, which holds the underlying value, and property, which provides the proof that val satisfies p.

Equality of elements in subtypes

Subtypes have a notion of equality based on that of the original type. Specifically, two elements of type Subtype P are equal if and only if their corresponding values in A are also equal. For this we have the the theorems Subtype.eq and Subtype.eq_iff.

SubtypeEq.lean

#check Subtype.eq     -- `a1.val = a2.val → a1 = a2`
#check Subtype.eq_iff -- `a1.val = a2.val ↔ a1 = a2`