[Solved]: Standard constructive definitions of integers, rationals, and reals?

There are multiple ways to define a mathematical structure, depending on what properties you consider to be the definition. Between equivalent characterizations, which one you take to be the definition and which one you take to be an alternative characterization is not important. In constructive mathematics, it is preferable to pick a definition that makes constructive reasoning easy. For natural numbers, the basic form of reasoning is induction, which makes the traditional zero-or-successor definition very much suitable. Other sets of numbers don’t have such a preference. When reasoning on quotients, in non-constructive settings, it is common to say “pick a member of the equivalence class”. In a constructive setting, it is necessary to describe how to pick a member. This makes it easier to go with definitions that construct one object for each member of the type, rather than constructing equivalence classes. For example, to define $mathbb{Z}$, a mathematician might be happy with equating differences of natural numbers: $$mathbb{Z} := mathbb{N}^2 / {((x,y),(x’,y’)) mid x + y’ = x’ + y}$$ While this has a tidy feeling to it (no “this or that”), for constructive reasoning, it’s simpler if equality of objects coincides with equality of representations, so we might define the relative integers as either a natural number or the negative of a natural number minus one:

Inductive Z1 :=   | Nonnegative : nat -> Z1   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)   | Negative : nat -> Z1.     (* ⟦Negative x⟧ = -⟦x⟧-1 *) 

However, this definition is oddly asymmetric, which can make it preferable to admit two different representations for zero:

Inductive Z2 :=   | Nonnegative : nat -> Z2   (* ⟦Nonnegative x⟧ = ⟦x⟧ *)   | Nonpositive : nat -> Z2.  (* ⟦Nonpostitive x⟧ = -⟦x⟧ *) 

Or we can build the relative integers without using the naturals as a building block:

Inductive Pos3 :=   | I : Pos3                  (* ⟦I⟧ = 1 *)   | S3 : Pos3 -> Pos3         (* ⟦S3 x⟧ = ⟦x⟧+1 *) Inductive Z3 :=   | N3 : Pos3 -> Z3           (* ⟦N3 x⟧ = -⟦x⟧ *)   | O3 : Z3                   (* ⟦O3⟧ = 0 *)   | P3 : Pos3 -> Z3           (* ⟦P3 x⟧ = ⟦x⟧ *) 

The Coq standard library uses yet another definition: it constructs positive integers from their notation is base 2, as the digit 1 followed by a sequence of digits 0 or 1. It then constructs Z like Z3 from Pos3 above. This definition also has a unique representation for each integer. The choice of using binary notation is not for easier reasoning, but to produce more efficient code when programs are extracted from proofs. Ease of reasoning is a motivation in picking a definition, but it is never an insurmountable factor. If some construction makes a particular proof easier, one can use that definition in that particular proof, and prove that the construction is equivalent to the other construction that was chosen as the definition originally. For rational numbers, it’s difficult to escape quotients, unless we start from a representation of integers as a product of factors (which makes some fundamental operations such as addition and the total ordering on $mathbb{N}$ difficult to define). The Coq standard library defines Q as $mathbb{N} times mathbb{N}^*$ (numerator and denominator), and defines an operator =?= to test the equivalence of two elements of Q. This definition is pretty common because that’s as simple as it gets. Real numbers are a whole different kettle of fish because they are not constructible. It is impossible to define the real numbers as an inductive type (all inductive types are denumerable). Instead, any definition of the real numbers has to be axiomatic, i.e. non-constructive. It is possible to construct denumerable subsets of the real numbers; the way to do that depends on what subset you want to construct.