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.

Examples of subtypes

The False subtype

Given a type A, we can consider the False subtype on A.

False.lean

def SFalse {A : Type} := { a : A // PFalse a}

The True subtype

Given a type A, we can consider the True subtype on A.

True.lean

def STrue {A : Type} := { a : A // PTrue a}

The image of a function

We introduce the image of a function. Given two types A and B and a function f : A → B, we define the image of f, denoted as Im f, as the subtype of B consisting of all elements that are mapped from some a : A under f.

Image.lean

def Im {A B : Type} (f : A → B) : Type := { b : B // ∃ (a : A), f a = b}

Elements of a subtype

To create an element of Subtype P, we use the Subtype.mk function, which maps an element a : A and a proof h : P a to an element of type Subtype P.

Subtype.lean

variable (a : A)
variable (h : P a)
#check Subtype.mk a h 

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.

SubtypeEqElem.lean

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

The inclusion function

The inclusion function is a function of a subtype into its underlying type: it simply extracts the value of a Subtype P element, discarding its proof.

Inclusion.lean

def inc {A : Type} {P : A → Prop} : Subtype P → A := by
  intro a
  exact a.val

Thanks to Subtype.eq we can prove that the inclusion function is always injective.

Inclusion.lean

theorem Tincinj {A : Type} {P : A → Prop} : injective (@inc A P) := by
  intro a1 a2 h1
  exact Subtype.eq h1

Functions and Subtypes

Restriction

We can formalize the notion of restricting functions to subtypes. Any function f : A → B can be restricted to a subtype by applying f only to the underlying values of the subtype elements. Restriction provides a way to transform elements of type A → B into elements of type Subtype P → B.

Restriction.lean

def rest {A B : Type} {P : A → Prop} (f : A → B) : Subtype P → B := by
  intro a
  exact f a.val

Correstriction

Given a function f : A → B and a predicate Q on B, we can correstrict f to Subtype P, provided that every b : Im f satisfies Q. If the above condition holds, correstriction provides a way to transform elements of type A → B into elements of type A → Subtype Q.

Correstriction.lean

def correst {A B : Type} {Q : B → Prop} (f : A → B) (h : ∀ (b : Im f), Q b.val) 
: A → Subtype Q := by
  intro a
  have ha : ∃ (a1 : A), f a1 = f a := by
    apply Exists.intro a
    exact rfl
  apply Subtype.mk (f a) (h ⟨f a, ha⟩)

Birrestriction

Given a function f : A → B, a predicate P on A and a predicate Q on B, we can birrestrict f to the respective subtypes, provided that f a satisfies Q for every a : Subtype P. If the above condition holds, birrestriction provides a way to transform elements of type A → B into elements of type Subtype P → Subtype Q.

Birrestriction.lean

def birrest {A B : Type} {P : A → Prop} {Q : B → Prop} (f : A → B) (h : ∀ (a : A), P a → Q (f a)) : Subtype P → Subtype Q := by
  apply correst (rest f)
  intro ⟨b, ⟨a, ha⟩⟩
  simp
  specialize h a.val
  have hb : f a.val = b := ha
  rw [hb] at h
  exact h a.property

In particular, given two predicates P1 and P2 on a type A, the following function establishes a transformation from the subtype corresponding to P1 to the subtype corresponding to P2, provided that P1 implies P2. This is achieved by birrestricting the identity function.

SubtoSub.lean

def SubtoSub {A : Type} {P1 P2 : A → Prop} (h : ∀ (a : A), P1 a → P2 a) : 
Subtype P1 → Subtype P2 := birrest id h

Equalizers

In this section, we introduce the concept of the equalizer of two functions, a construction that identifies the subtype of a domain where the two functions agree. Beyond its definition as a subtype, the equalizer is also characterized by a universal property: it serves as the most general type equipped with a map into A on which the functions agree.

Given two functions f, g : A → B, the equalizer of f and g is the subtype of A consisting on all elements a : A such that f a = g a.

Equalizer.lean

def Eq {A B : Type} (f g : A → B) : Type := { a : A // f a = g a}

It commes equipped with the inclusion function, from the equalizer to A.

Equalizer.lean

def incEq {A B : Type} (f g : A → B) : Eq f g → A := @inc A (fun a => f a = g a) 

This inclusion satisfies that f ∘ (incEq f g) = g ∘ (incEq f g).

Equalizer.lean

theorem TEqInc {A B : Type} (f g : A → B) : f ∘ (incEq f g) = g ∘ (incEq f g) := by
  apply funext
  intro a
  calc
    (f ∘ (incEq f g)) a = f a.val             := rfl
    _                   = g a.val             := a.property
    _                   = (g ∘ (incEq f g)) a := rfl

Universal property of the equalizer

The universal property of the equalizer characterizes it not merely as a subtype, but as a universal solution to the problem of mediating between f and g. The universal property states that the pair (Eq, inc) is initial among all pairs (C, h), where C is a type and h : C → A is a function satisfying f ∘ h = g ∘ h.

That is, if C is a type and h : C → A is a function satisfying f ∘ h = g ∘ h, then there exists a unique function u : C → Eq such that inc ∘ u = h.

Equalizer.lean

-- If there is another function `h : C → A` satisfying
-- `f ∘ h = g ∘ h`, then there exists a function `u : C → Eq f g`
def u {A B C : Type} {f g : A → B} {h : C → A} (h1 : f ∘ h = g ∘ h) : C → Eq f g := by
  intro c
  exact Subtype.mk (h c) (congrFun h1 c)

-- The function `u` satisfies that `incEq f g ∘ u = h`
theorem TEqIncEq {A B C : Type} {f g : A → B} {h : C → A} (h1 : f ∘ h = g ∘ h) : 
(incEq f g) ∘ (u h1) = h := by
  apply funext
  intro c
  exact rfl

-- The function `u` is unique in the sense that, if there is another function 
-- `v : C → Eq f g` satisfying `incEq f g ∘ v = h`, then `v = u`.
theorem TEqUni {A B C : Type} {f g : A → B} {h : C → A} (h1 : f ∘ h = g ∘ h) 
(v : C → Eq f g) (h2 : (incEq f g) ∘ v = h) : v = u h1 := by
  apply funext
  intro c
  apply Subtype.eq
  calc
    (v c).val = ((incEq f g) ∘ v) c := rfl
    _         = h c                 := congrFun h2 c
    _         = (u h1 c).val        := rfl

In other words, any function into A that “equalizes” f and g factors uniquely through the equalizer. This property ensures that the equalizer is the most general and canonical way to capture the elements where two functions agree.

Exercises

Subtypes

Exercises.lean

-- If two subtypes are equivalent, the corresponding subtypes are equal.
theorem TEqSubtype {A : Type} {P1 P2 : A → Prop} 
(h : ∀ (a : A), P1 a ↔ P2 a) : Subtype P1 = Subtype P2 := by sorry

Restriction

Exercises.lean

-- Im (inc) = Subtype
theorem TUPSub {A : Type} {P : A → Prop} : Im (@inc A P) = Subtype P := by sorry

-- `rest f = f ∘ inc`
theorem TRest {A B : Type} {f : A → B} {P : A → Prop}: (@rest A B P f) = 
f ∘ (@inc A P) := by sorry

Correstriction

Theorems TUPCorrest and TUPCorrestUn establish the universal property of the correstriction of a function. The first result, TUPCorrest, states that for any function f : A → B that respects a predicate Q on B (i.e., Q b holds for all b : Im f)), the function f can be expressed as the composition of the inclusion function inc and its correstriction correst f h, that is f = inc ∘ (correst f h). The second result, TUPCorrestUn, establishes the uniqueness of the correstriction. If there exists another function g : A → Subtype P such that f = inc ∘ g, then g must be exactly correst f h.

Exercises.lean

-- f = inc ∘ correst
theorem TUPCorrest {A B : Type} {Q : B → Prop} {f : A → B} 
(h : ∀ (b : Im f), Q b.val) : f = (@inc B Q) ∘ (correst f h) := by sorry
  
-- Unicity
theorem TUPCorrestUn {A B : Type} {Q : B → Prop} {f : A → B} 
(h : ∀ (b : Im f), Q b.val) (g : A → Subtype Q) (h1 : f = (@inc B Q) ∘ g) 
: (correst f h) = g := by sorry

Equalizers

Exercises.lean

-- The function `incEq` is a monomorphism
theorem TincEqMono {A B : Type} {f g : A → B} : monomorphism (incEq f g) := by sorry
  
-- An epic `incEq` is an isomorphism
theorem TincEqEpi {A B : Type} {f g : A → B} : epimorphism (incEq f g) → 
isomorphism (incEq f g) := by sorry