module Data.Int.Base where

# The integersπ

The familiar set of integers, in addition to its intuitive characterisation in terms of positive and negative numbers, can be specified by a wide variety of universal properties:

The set of integers, with the operation of addition, is the free group on one generator (see the group of integers).

The set of integers, with the operations of addition and multiplication, is the initial ring.

The set of integers under addition, considered together with the embedding $NβͺZ$ of the positive numbers, is the free group generated by the

*monoid*of natural numbers.The set of integers is the loop space of the circle. More generally, it appears (as a group under addition) as the first non-trivial higher homotopy group of all spheres: $Ο_{n}(S_{n})βZ.$

The set of integers, with the number zero and the successor equivalence, is the initial pointed type with an equivalence.

All of these specifications can be turned into code, and regardless
of your choice, it would be provably equivalent to any of the others.
Therefore, there is no *mathematical* reason to pick one over the
others. However, the real world imposes two constraints on us:
convenience and efficiency.

On the convenience front, itβs simply more convenient to formalise
further results if there is a definition of the integers which we take
as *the* definition. And, since this definition will be
ubiquitous, itβs best if it has compact normal forms for numbers, and
supports definition of the relevant structure in a computationally nice
way.

For definiteness, we go with the most elementary, inductive representation:

data Int : Type where pos : Nat β Int negsuc : Nat β Int

{-# BUILTIN INTEGER Int #-} {-# BUILTIN INTEGERPOS pos #-} {-# BUILTIN INTEGERNEGSUC negsuc #-} pattern posz = pos zero pattern possuc x = pos (suc x)

The definition above is isomorphic to a sum type, where both summands
are the natural numbers. However, if we interpret this naΓ―vely, then we
would have a problem: there are now two copies of the number zero! This
is, essentially, a problem of *intent*. We have to choose one of
the two summands to contain the number zero, and the names we choose for
the constructors must reflect this.

The constructor `pos`

embeds the
positive numbers β incl. zero! β while the constructor `negsuc`

constructs
the **neg**ation of a **succ**essor. This
means that `negsuc 0`

is the
representation of the number
$β1.$

Other than these constructors, we can define a difference operation, between natural numbers, valued in the integers. This difference correctly reflects, in its sign, whether we tried to subtract a large quantity from a smaller quantity.

_β-_ : Nat β Nat β Int x β- zero = pos x zero β- suc y = negsuc y suc x β- suc y = x β- y

We can also use this to demonstrate the offsetting built into `negsuc`

:

_ : 0 β- 20 β‘ negsuc 19 _ = refl

pos-injective : β {x y} β pos x β‘ pos y β x β‘ y pos-injective = ap (case_of Ξ» { (pos x) β x ; (negsuc _) β zero }) negsuc-injective : β {x y} β negsuc x β‘ negsuc y β x β‘ y negsuc-injective = ap (case_of Ξ» { (pos x) β 0 ; (negsuc x) β x }) posβ negsuc : β {x y} β pos x β‘ negsuc y β β₯ posβ negsuc p = subst (Ξ» { (pos x) β β€ ; (negsuc _) β β₯ }) p tt negsucβ pos : β {x y} β negsuc x β‘ pos y β β₯ negsucβ pos p = posβ negsuc (sym p) _ = Discrete-Nat

## Equalityπ

We mentioned in the introductory paragraph that the type of integers is a set. We will show something stronger: itβs actually discrete. This means that we have a procedure that can tell whether two integers are equal, and produce a refutation when they are not equal. Intuitively, this is because the natural numbers are discrete, and itβs embedded in the integers.

The first thing to do is discriminate between the two constructors. If they match, we can compare the underlying natural numbers:

instance Discrete-Int : Discrete Int Discrete-Int {pos x} {pos y} with x β‘? y ... | yes p = yes (ap pos p) ... | no Β¬p = no Ξ» path β Β¬p (pos-injective path) Discrete-Int {negsuc x} {negsuc y} with x β‘? y ... | yes p = yes (ap negsuc p) ... | no Β¬p = no Ξ» path β Β¬p (negsuc-injective path)

If theyβre mismatched, we have pre-existing refutations.

Discrete-Int {pos x} {negsuc y} = no posβ negsuc Discrete-Int {negsuc x} {pos y} = no negsucβ pos

Number-Int : Number Int Number-Int .Number.Constraint _ = β€ Number-Int .Number.fromNat n = pos n Negative-Int : Negative Int Negative-Int .Negative.Constraint _ = β€ Negative-Int .Negative.fromNeg zero = pos zero Negative-Int .Negative.fromNeg (suc x) = negsuc x opaque H-Level-Int : β {n} β H-Level Int (2 + n) H-Level-Int = basic-instance 2 (Discreteβis-set Discrete-Int)

## As the universal symmetryπ

One of the mentioned characterisations of the integers was as the initial type
equipped with a point and an auto-equivalence. This equivalence is the
*successor* function: if we picture the integers as a number
line, the effect of this equivalence is to βrotateβ the line to the
right.

sucβ€ : Int β Int sucβ€ (pos n) = pos (suc n) sucβ€ (negsuc zero) = 0 sucβ€ (negsuc (suc n)) = negsuc n predβ€ : Int β Int predβ€ (pos zero) = -1 predβ€ (pos (suc n)) = pos n predβ€ (negsuc n) = negsuc (suc n)

The definition of the successor and predecessor functions is slightly complicated by the need to adjust by one when passing between the summands. The proof that these are inverses is a case bash precisely mirroring the structure of the functions.

suc-predβ€ : (x : Int) β sucβ€ (predβ€ x) β‘ x suc-predβ€ (negsuc x) = refl suc-predβ€ (pos zero) = refl suc-predβ€ (pos (suc x)) = refl pred-sucβ€ : (x : Int) β predβ€ (sucβ€ x) β‘ x pred-sucβ€ (pos x) = refl pred-sucβ€ (negsuc zero) = refl pred-sucβ€ (negsuc (suc x)) = refl suc-equiv : Int β Int suc-equiv = IsoβEquiv (sucβ€ , iso predβ€ suc-predβ€ pred-sucβ€)

## As signed numbersπ

Considering the isomorphism
$X+Xβ2βX,$
we arrive at an equivalent representation of the integers: as a pair
consisting of a natural number and its *sign*. We have
projections
$Zβ+,β$
and
$ZβN$
which correspond to this view: given an integer, we can determine its
sign and its **absolute value**.

data Sign : Type where pos neg : Sign abs : Int β Nat abs (pos x) = x abs (negsuc x) = suc x sign : Int β Sign sign (pos x) = pos sign (negsuc x) = neg

Conversely, if we have a signed number, we can build an integer. Note
that the `assign`

function sends the
natural number zero to the integer zero regardless of what sign is
specified.

assign : Sign β Nat β Int assign s zero = 0 assign pos (suc n) = pos (suc n) assign neg (suc n) = negsuc n

## Algebraπ

We also mentioned two more characterisations of the integers: as the free group on one generator, and as the initial ring. Therefore, we expect to find operations of addition, multiplication, and negation (additive inverse) on the set of integers. They are not that hard to define.

Addition on integers is defined by cases on the sign. If both numbers are positive (resp. negative), then we can compute their sum in the natural numbers. If the numbers have mismatched sign, then the addition function is actually computing a difference, and we already know how to compute differences.

_+β€_ : Int β Int β Int pos x +β€ pos y = pos (x + y) pos x +β€ negsuc y = x β- suc y negsuc x +β€ pos y = y β- suc x negsuc x +β€ negsuc y = negsuc (suc (x + y))

The negation function is defined by a short case bash. Subtraction is defined as addition against the inverse, rather than as an operation in its own right.

negβ€ : Int β Int negβ€ (pos zero) = pos zero negβ€ (pos (suc x)) = negsuc x negβ€ (negsuc x) = pos (suc x) _-β€_ : Int β Int β Int x -β€ y = x +β€ (negβ€ y)

The implementation of multiplication uses the decomposition of numbers into their signs and absolute values: The product $xy$ is defined to be

$sign(x)βsign(y)ββ£xβ£ββ£yβ£,$There are actually three different βmultiplicationβ signs in the
formula above. The first is *sign multiplication*, the second is
`assign`

, and the last is natural
number multiplication.

signΓ : Sign β Sign β Sign signΓ pos pos = pos signΓ neg neg = pos signΓ pos neg = neg signΓ neg pos = neg _*β€_ : Int β Int β Int i@(pos _) *β€ j = assign (signΓ pos (sign j)) (abs i * abs j) i@(negsuc _) *β€ j = assign (signΓ neg (sign j)) (abs i * abs j)

There are actually alternative definitions of addition and
multiplication: as iterated successor/predecessor, and as iterated
addition, respectively. These alternative representations have worse
*performance*, but they behave in a way that is slightly easier
to reason about. When establishing the algebraic properties of the
integers, weβll prove that these functions are equivalent to the
definitions above, and change between them as appropriate.

rotβ€ : Int β Int β Int rotβ€ (pos zero) y = y rotβ€ (pos (suc x)) y = sucβ€ (rotβ€ (pos x) y) rotβ€ (negsuc zero) y = predβ€ y rotβ€ (negsuc (suc x)) y = predβ€ (rotβ€ (negsuc x) y) dotβ€ : Int β Int β Int dotβ€ posz y = posz dotβ€ (possuc x) y = y +β€ (dotβ€ (pos x) y) dotβ€ (negsuc zero) y = negβ€ y dotβ€ (negsuc (suc x)) y = negβ€ y +β€ (dotβ€ (negsuc x) y)

## Additional operationsπ

It is also straightforward to define maximum and minimum operations for integers:

maxβ€ : Int β Int β Int maxβ€ (pos x) (pos y) = pos (max x y) maxβ€ (pos x) (negsuc _) = pos x maxβ€ (negsuc _) (pos y) = pos y maxβ€ (negsuc x) (negsuc y) = negsuc (min x y) minβ€ : Int β Int β Int minβ€ (pos x) (pos y) = pos (min x y) minβ€ (pos _) (negsuc y) = negsuc y minβ€ (negsuc x) (pos _) = negsuc x minβ€ (negsuc x) (negsuc y) = negsuc (max x y)

data Positive : Int β Type where pos : β x β Positive (possuc x) instance H-Level-Positive : β {n k} β H-Level (Positive n) (suc k) H-Level-Positive {n} = prop-instance (retractβis-hlevel 1 (from _) (to _) (li _) (isp n)) where pos' : Int β Type pos' posz = β₯ pos' (possuc x) = β€ pos' (negsuc x) = β₯ isp : β n β is-prop (pos' n) isp (possuc _) tt tt = refl to : β x β Positive x β pos' x to .(possuc x) (pos x) = tt from : β x β pos' x β Positive x from (possuc x) tt = pos x li : β x β is-left-inverse (from x) (to x) li .(possuc x) (pos x) = refl Positive-suc : β {x} β Positive (possuc x) Positive-suc = pos _ Dec-Positive : β {x} β Dec (Positive x) Dec-Positive {posz} = no Ξ» () Dec-Positive {negsuc x} = no Ξ» () Dec-Positive {possuc x} = yes (pos x)