Requesting review: ℕ, ℤ and ℚ implemented from scratch

Stream: new members

[Isak Colboubrani]

I have defined the natural numbers, the integers, and the rational numbers in Lean 4, although I relied on some liberal use of sorry and referenced existing code. My aim has been to construct these number systems as they are typically defined in undergraduate mathematics. The goal is to use these as building blocks for defining the real numbers next (I understand that this will be significantly more challenging than what I've done so far!).

I would appreciate a review of the following definitions/setup. Please let me know if anything seems odd, if there are more idiomatic ways to express these definitions, or if any improvements can be made. Is there anything essential that I might have overlooked, which will be needed for the next step of defining the real numbers? Anything redundant or unnecessary? I am eager to learn from your feedback, so feel free to be meticulous!

I used the traditional approach to define the natural numbers as a Peano structure:

inductive nat
  | zero : nat
  | succ (n : nat) : nat

The integers are defined as pairs of natural numbers:

structure int_pair where
  plus : nat
  minus : nat
…
def int : Type := Quotient int_pair_setoid
…
def int.mk (z : int_pair) : int := int.normalize <| Quotient.mk int_pair_setoid z

The rational numbers are defined as pairs of integers:

structure rat_pair where
  numerator : int
  denominator : int
…
def rat : Type := Quotient rat_pair_setoid
…
def rat.mk (z : rat_pair) : rat := rat.normalize <| Quotient.mk rat_pair_setoid z

In addition to the above, I have defined:

def nat.add (n1 n2 : nat) : nat
def nat.pred : nat → nat
def nat.sub : nat → nat → nat
inductive nat.le (n : nat) : nat → Prop
def nat.lt (n m : nat) : Prop
def nat.ble : nat → nat → Bool
def nat.div (x y : nat) : nat
def nat.mul (n1 n2 : nat) : nat
def nat.mod (x y : nat) : nat
def nat.gcd : nat → nat → nat

def int.normalize (z : int) : int
def int.mk (z : int_pair) : int
def int.add (z1 z2 : int) : int
def int.mul (z1 z2 : int) : int
def int.neg (z : int) : int
def int.abs (z : int) : nat
def int.is_negative (z : int) : Bool

def rat.normalize (z : rat) : rat
def rat.mk (z : rat_pair) : rat
def rat.add (z1 z2 : rat) : rat
def rat.mul (z1 z2 : rat) : rat
def rat.neg (z : rat) : rat
def rat.inv (z : rat) : rat

With the following setup:

instance : Add nat where add := nat.add
instance : LE nat where le := nat.le
instance : LT nat where lt := nat.lt
instance : Trans (. < . : nat → nat → Prop) (. < . : nat → nat → Prop) (. < . : nat → nat → Prop) where …
instance : Trans (. ≤ . : nat → nat → Prop) (. ≤ . : nat → nat → Prop) (. ≤ . : nat → nat → Prop) where …
instance : Trans (. < . : nat → nat → Prop) (. ≤ . : nat → nat → Prop) (. < . : nat → nat → Prop) where …
instance : Trans (. ≤ . : nat → nat → Prop) (. < . : nat → nat → Prop) (. < . : nat → nat → Prop) where …
instance nat.decLe (n m : nat) : Decidable (LE.le n m) := …
instance nat.decLt (n m : nat) : Decidable (LT.lt n m) := …
instance : Mul nat where mul := nat.mul
instance : Mod nat where mod := nat.mod

instance : Setoid int_pair := int_pair_setoid
instance : Add int where add := int.add
instance : Mul int where mul := int.mul
instance : Neg int where neg := int.neg
instance : Coe nat int where coe n := int.mk { plus := n, minus := 0 }
instance : Repr int where …

instance : Setoid rat_pair := rat_pair_setoid
instance : Add rat where add := rat.add
instance : Mul rat where mul := rat.mul
instance : Neg rat where neg := rat.neg
instance : Inv rat where inv := rat.inv
instance : Coe int rat where coe i := rat.mk { numerator := i, denominator := 1 }
instance : Repr rat where …

[Kevin Buzzard]

What is your definition of rat_pair_setoid? What is rat.mk \<1, 0\>?

[Isak Colboubrani]

Oh, good point! That's one of my unresolved issues: currently, I'm allowing the denominator in the rat construction to be zero (rat.mk ⟨i, 0⟩). Unlike Mathlib, I think I want to disallow this to avoid potential pitfalls.

Currently, rat.mk ⟨i, 0⟩ (for any i) is normalized to rat.mk ⟨1, 0⟩, unlike in Mathlib, where I believe it is normalized to rat.mk ⟨0, 0⟩?

This is my current rat setup:

structure rat_pair where
  numerator : int
  denominator : int
def rat_pair_relation (ab cd : rat_pair) : Prop := ab.numerator * cd.denominator = cd.numerator * ab.denominator
def rat_pair_setoid : Setoid rat_pair := Setoid.mk rat_pair_relation sorry
instance : Setoid rat_pair := rat_pair_setoid
def rat : Type := Quotient rat_pair_setoid

def rat.normalize (z : rat) : rat :=
  let numerator : int := int.normalize <| Quotient.liftOn z (fun x => x.numerator) sorry
  let numerator_without_sign : nat := int.abs numerator

  let denominator : int := int.normalize <| Quotient.liftOn z (fun x => x.denominator) sorry
  let denominator_without_sign : nat := int.abs denominator

  let greatest_common_denominator : nat := nat.gcd numerator_without_sign denominator_without_sign

  let numerator_normalized_without_sign : int := int.mk { plus := nat.div numerator_without_sign greatest_common_denominator, minus := 0 }
  let numerator_normalized_with_sign : int := (if int.is_negative numerator then -1 else 1) * numerator_normalized_without_sign
  let denominator_normalized : int := int.mk { plus := nat.div denominator_without_sign greatest_common_denominator, minus := 0 }

  Quotient.mk rat_pair_setoid { numerator := numerator_normalized_with_sign, denominator := denominator_normalized }

def rat.mk (z : rat_pair) : rat := rat.normalize <| Quotient.mk rat_pair_setoid z

[Mario Carneiro]

in mathlib, mkRat i 0 is normalized to Rat.mk 0 1 _ _, that is, numerator 0 and denominator 1 which is the normal form of 0

[Mario Carneiro]

in particular, Rat.mk requires that the denominator is nonzero. The division by zero behavior is instead encoded in the behavior of /, mkRat and other division-like operators producing Rat

[Kevin Buzzard]

def rat_pair_relation (ab cd : rat_pair) : Prop := ab.numerator * cd.denominator = cd.numerator * ab.denominator
def rat_pair_setoid : Setoid rat_pair := Setoid.mk rat_pair_relation sorry

This sorry is false, right? So your setup is inconsistent right now (meaning you can prove any statement from your assumptions, even false ones).

[Kevin Buzzard]

$(1,1)\sim(0,0)\sim(0,1)$ but $(1,1)\not\sim(0,1)$.

[Kevin Buzzard]

import Mathlib.Tactic

abbrev int := ℤ

structure rat_pair where
  numerator : int
  denominator : int

def rat_pair_relation (ab cd : rat_pair) : Prop := ab.numerator * cd.denominator = cd.numerator * ab.denominator
def rat_pair_setoid : Setoid rat_pair := Setoid.mk rat_pair_relation sorry -- now we can prove anything

lemma false : False := by
  match h : rat_pair_setoid with
  | ⟨r, hr⟩ =>
    cases h
    obtain ⟨refl, symm, trans⟩ := hr
    unfold rat_pair_relation at trans
    have h := @trans ⟨1,1⟩ ⟨0,0⟩ ⟨0,1⟩ (by simp) (by simp)
    norm_num at h

theorem FLT (a b c n : ℕ) : a^n + b^n ≠ c^n := false.elim

#print axioms FLT
-- 'FLT' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]

[Ruben Van de Velde]

All done!

[Isak Colboubrani]

Thank you very much for pointing out the issue with the relation, Kevin, and thank you, Ruben, for providing an excellent code illustration of the problem. I suspected that my liberal, although temporary, use of sorry would catch up with me eventually. This has been a great learning experience. Thanks again!

I've now implemented the following changes:

I changed from …

def rat_pair_relation (ab cd : rat_pair) : Prop :=
    ab.numerator * cd.denominator = cd.numerator * ab.denominator

… to …

def rat_pair_relation (ab cd : rat_pair) : Prop :=
    ab.numerator * cd.denominator = cd.numerator * ab.denominator ∧
    cd.denominator ≠ 0 ∧
    ab.denominator ≠ 0

And from …

structure rat_pair where
  numerator : int
  denominator : int

… to …

structure rat_pair where
  numerator : int
  denominator : int
  denominator_non_zero : denominator ≠ 0 := by decide

Is this approach correct? Are there any outstanding consistency issues?

[Kevin Buzzard]

The easiest way to find out if there are consistency issues is to try to fill in your own sorrys! They're only basic arithmetic. Oh but I guess this is hard for you because you're proving everything from scratch.

It seems to me that your current assumptions on nonzero denominator in rat_pair_relation are superfluous because they're already in rat_pair. But mathematically this looks much better.