⚠️ This module is not part of this project and is only included for reference.
It is either part of the 1lab, the cubical library, or a built-in Agda module.
<!--
```
open import 1Lab.Path.IdentitySystem
open import 1Lab.HLevel.Retracts
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type
open import Data.Dec.Base
open import Data.Nat.Base
```
-->
```agda
module Data.Int.Base where
```
# The integers {defines=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.
- 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 $\bN \mono \bZ$ 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: $\pi_n(\bS^n) \cong
\bZ$.
- The set of integers, with the number zero and the successor
equivalence, is the [initial pointed type with an
equivalence](Data.Int.Universal.html).
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:
```agda
data Int : Type where
pos : Nat → Int
negsuc : Nat → Int
```
<!--
```agda
{-# 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`{.Agda} embeds the positive numbers --- incl. zero!
--- while the constructor `negsuc`{.Agda} constructs the **neg**ation of
a **succ**essor. This means that `negsuc 0`{.Agda} 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.
```agda
_ℕ-_ : 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`{.Agda}:
```agda
_ : 0 ℕ- 20 ≡ negsuc 19
_ = refl
```
<!--
```agda
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|embedding]] in the integers.
The first thing to do is discriminate between the two constructors. If
they match, we can compare the underlying natural numbers:
```agda
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.
```agda
Discrete-Int {pos x} {negsuc y} = no pos≠negsuc
Discrete-Int {negsuc x} {pos y} = no negsuc≠pos
```
<!--
```agda
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|initial object]] 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.
```agda
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.
```agda
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 \cong 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 $\bZ \to {+,-}$ and
$\bZ \to \bN$ which correspond to this view: given an integer, we can
determine its sign and its **absolute value**.
```agda
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`{.Agda} function sends the natural number zero to the
integer zero regardless of what sign is specified.
```agda
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.
```agda
_+ℤ_ : 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.
```agda
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
$$
\operatorname{sign}(x) * \operatorname{sign}(y) * |x| * |y|\text{,}
$$
There are actually three different "multiplication" signs in the formula
above. The first is _sign multiplication_, the second is
`assign`{.Agda}, and the last is natural number multiplication.
```agda
sign× : Sign → Sign → Sign
sign× pos pos = pos
sign× neg neg = pos
sign× pos neg = neg
sign× neg pos = neg
_*ℤ_ : Int → Int → Int
i *ℤ j = assign (sign× (sign i) (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.
```agda
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:
```agda
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)
```