Quotient types allow a new type to be formed by decreasing the granularity of an existing type's propositional equality.
In particular, given an type A and an equivalence relation \sim, the quotient A / \sim contains the same elements as A, but every pair of elements that are related by \sim are considered equal.
Equality is respected universally; nothing in Lean's logic can observe any difference between two equal terms.
Thus, quotient types provide a way to build an impenetrable abstraction barrier.
In particular, all functions from a quotient type must prove that they respect the equivalence relation.
Quotient types coarsen the propositional equality for a type so that terms related by some
equivalence relation are considered equal. The equivalence relation is given by an instance of
Setoid.
Set-theoretically, Quotients can seen as the set of equivalence classes of α modulo the
Setoid instance's relation s.r. Functions from Quotients must prove that they respect s.r:
to define a function f:Quotients→β, it is necessary to provide f':α→β and prove that
for all x:α and y:α, s.rxy→f'x=f'y. Quotient.lift implements this operation.
The key quotient operators are:
Quotient.mk places elements of the underlying type α into the quotient.
Quotient.lift allows the definition of functions from the quotient to some other type.
Quotient.sound asserts the equality of elements related by r
Quotient.ind is used to write proofs about quotients by assuming that all elements are
constructed with Quotient.mk.
Quotient is built on top of the primitive quotient type Quot, which does not require a proof
that the relation is an equivalence relation. Quotient should be used instead of Quot for
relations that actually are equivalence relations.
A proof that two elements of the underlying type are related by the equivalence relation is sufficient to prove that they are equal in the Quotient.
However, definitional equality is unaffected by the use of Quotient: two elements in the quotient are definitionally equal if and only if they are definitionally equal in the underlying type.
Quotient types are not widely used in programming.
However, they occur regularly in mathematics:
Integers
The integers are traditionally defined as a pair of natural numbers (n, k) that encodes the integer n - k.
In this encoding, two integers (n_1, k_1) and (n_2, k_2) are equal if n_1 + k_2 = n_2 + k_1.
Rational Numbers
The number \frac{n}{d} can be encoded as the pair (n, d), where d \neq 0.
Two rational numbers \frac{n_1}{d_1} and \frac{n_2}{d_2} are equal if n_1 d_2 = n_2 d_1.
Real Numbers
The real numbers can be represented as a Cauchy sequence, but this encoding is not unique.
Using a quotient type, two Cauchy sequences can be made equal when their difference converges to zero.
Finite Sets
Finite sets can be represented as lists of elements.
With a quotient types, two finite sets can be made equal if they contain the same elements; this definition does not impose any requirements (such as decidable equality or an ordering relation) on the type of elements.
One alternative to quotient types would be to reason directly about the equivalence classes introduced by the relation.
The downside of this approach is that it does not allow computation: in addition to knowing that there is an integer that is the sum of 5 and 8, it is useful for 5 + 8 = 13 to not be a theorem that requires proof.
Defining functions out of sets of equivalence classes relies on non-computational classical reasoning principles, while functions from quotient types are ordinary computational functions that additionally respect an equivalence relation.
While Quotient is a convenient way to form quotients with reasonable computational properties, it is often possible to define quotients in other ways.
In general, a type Q is said to be the quotient of A by an equivalence relation \sim if it respects the universal property of quotients: there is a function q:A\to Q with the property that q(a)=q(b) if and only if a\sim b for all a and b in A.
Quotients formed with Quotient have this property up to propositional equality: elements of A that are related by \sim are equal, so they cannot be distinguished.
However, members of the same equivalence class are not necessarily definitionally equal in the quotient.
Quotients may also be implemented by designating a single representative of each equivalence class in A itself, and then defining Q as pair of elements in A with proofs that they are such a canonical representative.
Together with a function that maps each a in A to its canonical representative, Q is a quotient of A.
Due to proof irrelevance, representatives in Q of the same equivalence class are definitionally equal.
Such a manually implemented quotient Q can be easier to work with than Quotient.
In particular, because each equivalence class is represented by its single canonical representative, there's no need to prove that functions from the quotient respect the equivalence relation.
It can also have better computational properties due to the fact that the computations give normalized values (in contrast, elements of Quotient can be represented in multiple ways).
Finally, because the manually implemented quotient is an inductive type, it can be used in contexts where other kinds of types cannot, such as when defining a nested inductive type.
However, not all quotients can be manually implemented.
Manually Quotiented Integers
When implemented as pairs of Nats, each equivalence class according to the desired equality for integers has a canonical representative in which at least one of the Nats is zero.
This can be represented as a Lean structure:
Due to proof irrelevance, every value of this structure type that represents the same integer is already equal.
Constructing a Z can be made more convenient with a wrapper that uses the fact that subtraction of natural numbers truncates at zero to automate the construction of the proof:
Because each equivalence class is uniquely represented, there's no need to write a proof that these functions from Z respect the equivalence relation.
However, in practice, the API for quotients should be implemented for manually-constructed quotients and proved to respect the universal property.
Built-In Integers as Quotients
Lean's built-in integer type Int satisfies the universal property of quotients, and can thus be thought of as a quotient of pairs of Nats.
The canonical representative of each equivalence class can be computed via comparison and subtraction:This toInt function is called Int.subNatNat in the standard library.
Quotient types are built on setoids.
A setoid is a type paired with a distinguished equivalence relation.
Unlike a quotient type, the abstraction barrier is not enforced, and proof automation designed around equality cannot be used with the setoid's equivalence relation.
Setoids are useful on their own, in addition to being a building block for quotient types.
An equivalence relation is a relation that is reflexive, symmetric, and transitive.
syntaxEquivalence Relations
Equivalence according to some canonical equivalence relation for a type is written using ≈, which is overloaded using the type classHasEquiv.
term::= ...
|`x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent.
Conventions for notations in identifiers:
* The recommended spelling of `≈` in identifiers is `equiv`.term≈term
The type Quotient expects an instance of Setoid as an ordinary parameter, rather than as an instance implicit parameter.
This helps ensure that the quotient uses the intended equivalence relation.
The instance can be provided either by naming the instance or by using inferInstance.
A value in the quotient is a value from the setoid's underlying type, wrapped in Quotient.mk.
Quotient.mk.{u} {α : Sort u} (s : Setoidα)
(a : α) : Quotients
Places an element of a type into the quotient that equates terms according to an equivalence
relation.
The setoid instance is provided explicitly. Quotient.mk' uses instance synthesis instead.
Given v:α, Quotient.mksv:Quotients is like v, except all observations of v's value
must respect s.r. Quotient.lift allows values in a quotient to be mapped to other types, so long
as the mapping respects s.r.
Places an element of a type into the quotient that equates terms according to an equivalence
relation.
The equivalence relation is found by synthesizing a Setoid instance. Quotient.mk instead expects
the instance to be provided explicitly.
Given v:α, Quotient.mk'v:Quotients is like v, except all observations of v's value
must respect s.r. Quotient.lift allows values in a quotient to be mapped to other types, so long
as the mapping respects s.r.
The Integers as a Quotient Type
The integers, defined as pairs of natural numbers where the represented integer is the difference of the two numbers, can be represented via a quotient type.
This representation is not unique: both (4,7) and (1,4) represent -3.
Two encoded integers should be considered equal when they are related by Z.eq:
Functions from quotients can be defined by proving that a function from the underlying type respects the quotient's equivalence relation.
This is accomplished using Quotient.lift or its binary counterpart Quotient.lift₂.
The variants Quotient.liftOn and Quotient.liftOn₂ place the quotient parameter first rather than last in the parameter list.
Quotient.lift.{u, v} {α : Sort u} {β : Sort v}
{s : Setoidα} (f : α → β) :
(∀ (a b : α), a ≈ b → fa = fb) →
Quotients → β
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's equivalence relation.
Given s:Setoidα and a quotient Quotients, applying a function f:α→β requires a proof
h that f respects the equivalence relation s.r. In this case, the function
Quotient.liftfh:Quotients→β computes the same values as f.
Quotient.liftOn is a version of this operation that takes the quotient value as its first explicit
parameter.
Quotient.liftOn.{u, v} {α : Sort u} {β : Sort v}
{s : Setoidα} (q : Quotients) (f : α → β)
(c : ∀ (a b : α), a ≈ b → fa = fb) : β
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's equivalence relation.
Given s:Setoidα and a quotient value q:Quotients, applying a function f:α→β requires
a proof c that f respects the equivalence relation s.r. In this case, the term
Quotient.liftOnqfh:β reduces to the result of applying f to the underlying α value.
Quotient.lift is a version of this operation that takes the quotient value last, rather than
first.
When the function's result type is a subsingleton, Quotient.recOnSubsingleton or Quotient.recOnSubsingleton₂ can be used to define the function.
Because all elements of a subsingleton are equal, such a function automatically respects the equivalence relation, so there is no proof obligation.
An alternative recursion or induction principle for quotients that can be used when the target type
is a subsingleton, in which all elements are equal.
In these cases, the proof that the function respects the quotient's equivalence relation is trivial,
so any function can be lifted.
Quotient.rec does not assume that the target type is a subsingleton.
The fundamental tools for proving properties of elements of quotient types are the soundness axiom and the induction principle.
The soundness axiom states that if two elements of the underlying type are related by the quotient's equivalence relation, then they are equal in the quotient type.
The induction principle follows the structure of recursors for inductive types: in order to prove that a predicate holds all elements of a quotient type, it suffices to prove that it holds for an application of Quotient.mk to each element of the underlying type.
Because Quotient is not an inductive type, tactics such as cases and induction require that Quotient.ind be specified explicitly with the using modifier.
The quotient axiom, which asserts the equality of elements related in the setoid.
Because Quotient is built on a lower-level type Quot, Quotient.sound is implemented as a
theorem. It is derived from Quot.sound, the soundness axiom for the lower-level quotient type
Quot.
A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with Quotient.mk.
Proofs About Quotients
Given the definition of integers as a quotient type from the prior examples, Quotient.ind and Quotient.sound can be used to prove that negation is an additive inverse.
First, Quotient.ind is used to replace instances of n with applications of Quotient.mk.
Having done so, the left side of the equality becomes definitionally equal to a single application of Quotient.mk, via unfolding definitions and the computation rule for Quotient.lift.
This makes Quotient.sound applicable, which yields a new goal: to show that both sides are related by the equivalence relation.
This is provable using simp_arith.
For more specialized use cases, Quotient.rec, Quotient.recOn, and Quotient.hrecOn can be used to define dependent functions from a quotient type to a type in any other universe.
Stating that a dependent function respects the quotient's equivalence relation requires a means of dealing with the fact that the dependent result type is instantiated with different values from the quotient on each side of the equality.
Quotient.rec and Quotient.recOn use the Quotient.sound to equate the related elements, inserting the appropriate cast into the statement of equality, while Quotient.hrecOn uses heterogeneous equality.
Quotient.rec.{u, v} {α : Sort u} {s : Setoidα}
{motive : Quotients → Sort v}
(f : (a : α) → motive (Quotient.mksa))
(h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ fa = fb)
(q : Quotients) : motiveq
A dependent recursion principle for Quotient. It is analogous to the
recursor for a structure, and can be used when the resulting type
is not necessarily a proposition.
While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
Quotient.lift is useful for defining non-dependent functions.
Quotient.ind is useful for proving theorems about quotients.
Quotient.recOn.{u, v} {α : Sort u}
{s : Setoidα} {motive : Quotients → Sort v}
(q : Quotients)
(f : (a : α) → motive (Quotient.mksa))
(h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ fa = fb) :
motiveq
A dependent recursion principle for Quotient. It is analogous to the
recursor for a structure, and can be used when the resulting type
is not necessarily a proposition.
While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
Quotient.lift is useful for defining non-dependent functions.
Quotient.ind is useful for proving theorems about quotients.
Like functions and universes, quotient types are a built-in feature of Lean's type system.
However, the underlying primitives are based on the somewhat simpler Quot type rather than on Quotient, and Quotient is defined in terms of Quot.
The primary difference is that Quot is based on an arbitrary relation, rather than a Setoid instance.
The provided relation need not be an equivalence relation; the rules that govern Quot and Eq automatically extend the provided relation into its reflexive, transitive, symmetric closure.
When the relation is already an equivalence relation, Quotient should be used instead of Quot so Lean can make use of the fact that the relation is an equivalence relation.
Low-level quotient types. Quotient types coarsen the propositional equality for a type α, so that
terms related by some relation r are considered equal in Quotr.
Set-theoretically, Quotr can seen as the set of equivalence classes of α modulo r. Functions
from Quotr must prove that they respect r: to define a function f:Quotr→β, it is
necessary to provide f':α→β and prove that for all x:α and y:α, rxy→f'x=f'y.
Quot.mk places elements of the underlying type α into the quotient.
Quot.lift allows the definition of functions from the quotient to some other type.
Quot.sound asserts the equality of elements related by r.
Quot.ind is used to write proofs about quotients by assuming that all elements are constructed
with Quot.mk.
The relation r is not required to be an equivalence relation; the resulting quotient type's
equality extends r to an equivalence as a consequence of the rules for equality and quotients.
When r is an equivalence relation, it can be more convenient to use the higher-level type
Quotient.
Quot.lift.{u, v} {α : Sort u} {r : α → α → Prop}
{β : Sort v} (f : α → β)
(a : ∀ (a b : α), rab → fa = fb) :
Quotr → β
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's relation.
Given a relation r:α→α→Prop and a quotient Quotr, applying a function f:α→β
requires a proof a that f respects r. In this case, Quot.liftfa:Quotr→β computes the
same values as f.
Quot.mk places elements of the underlying type α into the quotient.
Quot.sound asserts the equality of elements related by r
Quot.ind is used to write proofs about quotients by assuming that all elements are constructed
with Quot.mk; it is analogous to the recursor for a
structure.
The quotient axiom, which asserts the equality of elements related by the quotient's relation.
The relation r does not need to be an equivalence relation to use this axiom. When r is not an
equivalence relation, the quotient is with respect to the equivalence relation generated by r.
Quot.sound is part of the built-in primitive quotient type:
Quot.mk places elements of the underlying type α into the quotient.
Quot.lift allows the definition of functions from the quotient to some other type.
Quot.ind is used to write proofs about quotients by assuming that all elements are constructed
with Quot.mk; it is analogous to the recursor for a
structure.
Quotient types are described in more detail in the Lean Language
Reference.
In addition to the above constants, Lean's kernel contains a reduction rule for Quot.lift that causes it to reduce when used with Quot.mk, analogous to ι-reduction for inductive types.
Given a relation r over α, a function f from α to β, and a proof resp that f respects r, the term Quot.liftfresp(Quot.mkrx) is definitionally equal to fx.
Because Quot is not an inductive type, types implemented as quotients may not occur around nested occurrences in inductive type declarations.
These types declarations must be rewritten to remove the nested quotient, which can often be done by defining a quotient-free version and then separately defining an equivalence relation that implements the desired equality relation.
Nested Inductive Types and Quotients
The nested inductive type of rose trees nests the recursive occurrence of RoseTree under List:
However, taking a quotient of the List that identifies all elements in the style of squash types causes Lean to reject the declaration:
(kernel) arg #2 of 'SetTree.branch' contains a non valid occurrence of the datatypes being declaredinductiveSetTree(α:Typeu)where|leaf:α→SetTreeα|branch:Quot(fun(xsys:List(SetTreeα))=>True)→SetTreeα
(kernel) arg #2 of 'SetTree.branch' contains a non valid occurrence of the datatypes being declared
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's relation.
Given a relation r:α→α→Prop and a quotient's value q:Quotr, applying a f:α→β
requires a proof c that f respects r. In this case, Quot.liftOnqfh:β evaluates
to the result of applying f to the underlying value in α from q.
Quot.liftOn is a version of the built-in primitive Quot.lift with its parameters re-ordered.
Quotient types are described in more detail in the Lean Language
Reference.
Lean also provides convenient elimination from Quot into any subsingleton without further proof obligations, along with dependent elimination principles that correspond to those used for Quotient.
A dependent recursion principle for Quot. It is analogous to the
recursor for a structure, and can be used when the resulting type
is not necessarily a proposition.
While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
Quot.lift is useful for defining non-dependent functions.
Quot.ind is useful for proving theorems about quotients.
A dependent recursion principle for Quot that takes the quotient first. It is analogous to the
recursor for a structure, and can be used when the resulting type
is not necessarily a proposition.
While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
Quot.lift is useful for defining non-dependent functions.
Quot.ind is useful for proving theorems about quotients.
Because Lean's definitional equality includes a computational reduction rule for Quot.lift, quotient types are used in the standard library to prove function extensionality, which would need to be an axiom otherwise.
This is done by first defining a type of functions quotiented by extensional equality, for which extensional equality holds by definition.
Extensional functions can be applied just like ordinary functions.
Application respects extensional equality by definition: if applying to functions gives equal results, then applying them gives equal results.
To show that two functions that are extensionally equal are in fact equal, it suffices to show that the functions that result from extensionally applying the corresponding extensional functions are equal.
This is because
which is definitionally equal to funx=>fx, which is definitionally equal (by η-equivalence) to f.
A propositional version of the computation rule for Quot.lift would not suffice, because the reducible expression occurs in the body of a function and rewriting by an equality in a function would already require function extensionality.
From here, it is enough to show that the extensional versions of the two functions are equal.
This is true due to Quot.sound: the fact that they are in the quotient's equivalence relation is an assumption.
This proof is a much more explicit version of the one in the standard library:
Squash types are a quotient by the relation that relates all elements, transforming it into a subsingleton.
In other words, if α is inhabited, then Squashα has a single element, and if α is uninhabited, then Squashα is also uninhabited.
Unlike Nonemptyα, which is a proposition stating that α is inhabited and is thus represented by a dummy value at runtime, Squashα is a type that is represented identically to α.
Because Squashα is in the same universe as α, it is not subject to the restrictions on computing data from propositions.
The quotient of α by the universal relation. The elements of Squashα are those of α, but all
of them are equal and cannot be distinguished.
Squashα is a Subsingleton: it is empty if α is empty, otherwise it has just one element. It
is the “universal Subsingleton” mapped from α.
Nonemptyα also has these properties. It is a proposition, which means that its elements (i.e.
proofs) are erased from compiled code and represented by a dummy value. Squashα is a Typeu,
and its representation in compiled code is identical to that of α.
Consequently, Squash.lift may extract an α value into any subsingleton type β, while
Nonempty.rec can only do the same when β is a proposition.
Extracts a squashed value into any subsingleton type.
If β is a subsingleton, a function α→β cannot distinguish between elements of α and thus
automatically respects the universal relation that Squash quotients with.
