Defining Functions on Equivalence Classes

A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are equivalence classes: sets of equivalent concrete values. There are simple techniques for defining and reasoning about functions that operate on equivalence classes. A general lemma library is applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints.