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)