open import 1Lab.Path.IdentitySystem
open import 1Lab.HLevel.Closure
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Dec.Base
open import Data.Nat.Base hiding (Positive)

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 $\mathbb{N}\hookrightarrow \mathbb{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: ${\pi }_n({\mathbb{S}}^n)\cong \mathbb{Z}\text{.}$

• 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 negation of a successor. This means that negsuc 0 is the representation of the number $-1\text{.}$

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:

_ :  ℕ-  ≡ negsuc 
_ = 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) →  ; (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 ( + n)
    H-Level-Int = basic-instance  (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)    = 
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\cong 2\ast X\text{,}$ we arrive at an equivalent representation of the integers: as a pair consisting of a natural number and its sign. We have projections $\mathbb{Z}\to +,-$ and $\mathbb{Z}\to \mathbb{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    = 
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.

infixl  _+ℤ_ _-ℤ_
infixl  _*ℤ_

_+ℤ_ : 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

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  (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)