Two copies of Nat

With our construction of $\mathbb{Z}$, we (eventually) get two copies of $\mathbb{N}$ one coming from the function \(i : \mathbb{N} \to \mathbb{Z}\) and the other from \(j : \mathbb{N} \to \mathbb{Z}\)

We can think of one copy of $\mathbb{N}$ as the non-negative integers and the other as the non-positive integers – with their overlap being $0$.

One can could imagine building an inductive type from this expressing that we have two ways to build an integer from a natural number. Indeed, that is what Lean does but a slight shift. The two copies of Nat in Int are the non-negative integers and the strictly negative integers.

inductive Int : Type where
  | ofNat   : Nat → Int
  | negSucc : Nat → Int

negSucc n should be viewed as -n-1. Lean gives the analog of $j$ above as

def negOfNat : Nat → Int
  | 0      => 0
  | succ m => negSucc m

In Grothendieck construction of $\mathbb{Z}$, we got addition almost immediately since it was natural to add $\mathbb{N} \times \mathbb{N}$. In Lean, it requires a bit more book-keeping using successors when using negSucc.

def add (m n : Int) : Int :=
  match m, n with
  | ofNat m,   ofNat n   => ofNat (m + n)
  | ofNat m,   negSucc n => subNatNat m (succ n)
  | negSucc m, ofNat n   => subNatNat n (succ m)
  | negSucc m, negSucc n => negSucc (succ (m + n))

This uses subNatNat (read as subtract a natural number from a natural number).

def subNatNat (m n : Nat) : Int :=
  match (n - m : Nat) with
  | 0        => ofNat (m - n)  -- m ≥ n
  | (succ k) => negSucc k

Natural number subtraction returns 0 if m ≥ n.

On the other hand, perhaps multiplication looks simpler than the formula we had before.

def mul (m n : Int) : Int :=
  match m, n with
  | ofNat m,   ofNat n   => ofNat (m * n)
  | ofNat m,   negSucc n => negOfNat (m * succ n)
  | negSucc m, ofNat n   => negOfNat (succ m * n)
  | negSucc m, negSucc n => ofNat (succ m * succ n)