Andrew Sneap, November 2020 - March 2021

In this file I define rational numbers.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import Integers.Multiplication renaming (_*_ to _ℤ*_)
open import Integers.Negation
open import Integers.Order
open import Integers.Type
open import MLTT.Spartan renaming (_+_ to _∔_)
open import Naturals.HCF
open import Naturals.Multiplication renaming (_*_ to _ℕ*_)
open import Naturals.Properties
open import Notation.CanonicalMap
open import Rationals.Fractions
open import TypeTopology.SigmaDiscreteAndTotallySeparated
open import UF.DiscreteAndSeparated
open import UF.Sets
open import UF.Subsingletons

module Rationals.Type where

ℚ : 𝓤₀ ̇
ℚ = Σ q ꞉ 𝔽 , is-in-lowest-terms q

ℚ⁴ = ℚ × ℚ × ℚ × ℚ

is-in-lowest-terms-is-discrete : (q : 𝔽)
                               → is-discrete (is-in-lowest-terms q)
is-in-lowest-terms-is-discrete q α β
 = inl (is-in-lowest-terms-is-prop q α β)

ℚ-is-discrete : is-discrete ℚ
ℚ-is-discrete = Σ-is-discrete 𝔽-is-discrete is-in-lowest-terms-is-discrete

ℚ-is-set : is-set ℚ
ℚ-is-set = discrete-types-are-sets ℚ-is-discrete

to𝔽 : ℚ → 𝔽
to𝔽 (q , _) = q

toℚlemma : ((x , a) : 𝔽)
         → Σ ((x' , a') , p) ꞉ ℚ , (Σ h ꞉ ℕ , (x ＝ (pos (succ h)) ℤ* x')
                                            × (succ a ＝ (succ h) ℕ* succ a'))
toℚlemma (pos a , b) = f (divbyhcf a (succ b))
 where
  f : Σ h ꞉ ℕ , Σ x ꞉ ℕ , Σ y ꞉ ℕ , ((h ℕ* x ＝ a) × (h ℕ* y ＝ succ b))
                                  × coprime x y → _
  f (h , x , 0 , (γ₁ , γ₂) , r) = 𝟘-elim (positive-not-zero b (γ₂ ⁻¹))
  f (0 , x , succ y , (γ₁ , γ₂) , r) = 𝟘-elim (positive-not-zero b γ)
   where
    γ : succ b ＝ 0
    γ = succ b      ＝⟨ γ₂ ⁻¹                   ⟩
        0 ℕ* succ y ＝⟨ zero-left-base (succ y) ⟩
        0           ∎
  f (succ h , x , succ y , (γ₁ , γ₂) , r) = γ
   where
    I : pos a ＝ pos (succ h) ℤ* pos x
    I = pos a                 ＝⟨ ap pos γ₁ ⁻¹                                ⟩
        pos (succ h ℕ* x)     ＝⟨ pos-multiplication-equiv-to-ℕ (succ h) x ⁻¹ ⟩
        pos (succ h) ℤ* pos x ∎

    γ : _
    γ = ((pos x , y) , coprime-to-coprime' x (succ y) r) , h , I , (γ₂ ⁻¹)
toℚlemma (negsucc a , b) = f (divbyhcf (succ a) (succ b))
 where
  f : (Σ h ꞉ ℕ , Σ x ꞉ ℕ , Σ y ꞉ ℕ , ((h ℕ* x ＝ (succ a))
                               × (h ℕ* y ＝ succ b))
                               × coprime x y) → _
  f (h , x , 0 , (γ₁ , γ₂) , r) = 𝟘-elim (positive-not-zero b (γ₂ ⁻¹))
  f (h , 0 , succ y , (γ₁ , γ₂) , r) = 𝟘-elim (positive-not-zero a (γ₁ ⁻¹))
  f (0 , succ x , succ y , (γ₁ , γ₂) , r) = 𝟘-elim (positive-not-zero b γ)
   where
    γ : succ b ＝ 0
    γ = succ b      ＝⟨ γ₂ ⁻¹                   ⟩
        0 ℕ* succ y ＝⟨ zero-left-base (succ y) ⟩
        0 ∎
  f (succ h , succ x , succ y , (γ₁ , γ₂) , r) = γ
   where
    I : pos (succ a) ＝ (pos (succ h) ℤ* pos (succ x))
    I = pos (succ a)                 ＝⟨ ap pos γ₁ ⁻¹ ⟩
        pos (succ h ℕ* succ x)       ＝⟨ i            ⟩
        pos (succ h) ℤ* pos (succ x) ∎
     where
      i = pos-multiplication-equiv-to-ℕ (succ h) (succ x) ⁻¹

    II : negsucc a ＝ pos (succ h) ℤ* negsucc x
    II = negsucc a                       ＝⟨ ap -_ I ⟩
        - (pos (succ h) ℤ* pos (succ x)) ＝⟨ i       ⟩
        pos (succ h) ℤ* (- pos (succ x)) ∎
     where
      i = negation-dist-over-mult (pos (succ h)) (pos (succ x)) ⁻¹

    q : ℚ
    q = (negsucc x , y) , coprime-to-coprime' (succ x) (succ y) r

    γ : _
    γ = q , h , II , (γ₂ ⁻¹)

toℚ : 𝔽 → ℚ
toℚ q = pr₁ (toℚlemma q)

numℚ : 𝔽 → ℤ
numℚ q = (pr₁ ∘ pr₁ ∘ pr₁) (toℚlemma q)

dnomℚ : 𝔽 → ℕ
dnomℚ q = (pr₂ ∘ pr₁ ∘ pr₁) (toℚlemma q)

hcf𝔽 : 𝔽 → ℕ
hcf𝔽 q = pr₁ (pr₂ (toℚlemma q))

iltℚ : (q : 𝔽) → is-in-lowest-terms (numℚ q , dnomℚ q)
iltℚ (x , a) = (pr₂ ∘ pr₁) (toℚlemma (x , a))

numr : ((x , a) : 𝔽) → x ＝ (pos (succ (hcf𝔽 (x , a)))) ℤ* numℚ (x , a)
numr (x , a) = pr₁ (pr₂ (pr₂ (toℚlemma (x , a))))

dnomr : ((x , a) : 𝔽) → succ a ＝ succ (hcf𝔽 (x , a)) ℕ* succ (dnomℚ (x , a))
dnomr (x , a) = pr₂ (pr₂ (pr₂ (toℚlemma (x , a))))

dnomrP : ((x , a) : 𝔽)
       → pos (succ a) ＝ pos (succ (hcf𝔽 (x , a)) ℕ* succ (dnomℚ (x , a)))
dnomrP (x , a) = ap pos (dnomr (x , a))

dnomrP' : ((x , a) : 𝔽)
        → pos (succ a) ＝ pos (succ (hcf𝔽 (x , a))) ℤ* pos (succ (dnomℚ (x , a)))
dnomrP' (x , a) = γ
 where
  h  = hcf𝔽 (x , a)
  a' = dnomℚ (x , a)

  γ : pos (succ a) ＝ pos (succ h) ℤ* pos (succ a')
  γ = pos (succ a)                  ＝⟨ i  ⟩
      pos (succ h ℕ* succ a')       ＝⟨ ii ⟩
      pos (succ h) ℤ* pos (succ a') ∎
   where
    i  = dnomrP (x , a)
    ii = pos-multiplication-equiv-to-ℕ (succ h) (succ a') ⁻¹

0ℚ 1ℚ -1ℚ 1/3 2/3 1/2 1/5 2/5 3/5 1/4 3/4 : ℚ
-1ℚ = toℚ (negsucc 0 , 0)
0ℚ  = toℚ (pos 0 , 0)
1ℚ  = toℚ (pos 1 , 0)
1/3 = toℚ (pos 1 , 2)
2/3 = toℚ (pos 2 , 2)
1/2 = toℚ (pos 1 , 1)
1/5 = toℚ (pos 1 , 4)
2/5 = toℚ (pos 2 , 4)
3/5 = toℚ (pos 3 , 4)
4/5 = toℚ (pos 4 , 4)
1/4 = toℚ (pos 1 , 3)
3/4 = toℚ (pos 3 , 3)

equiv-equality : (p q : 𝔽) → p ≈ q ↔ toℚ p ＝ toℚ q
equiv-equality (x , a) (y , b) = γ₁ , γ₂
 where
  a' b' h h' : ℕ
  a' = dnomℚ (x , a)
  b' = dnomℚ (y , b)
  h  = hcf𝔽 (x , a)
  h' = hcf𝔽 (y , b)

  x' y' ph ph' pa' pb' : ℤ
  x'  = numℚ (x , a)
  y'  = numℚ (y , b)
  ph  = (pos ∘ succ) h
  ph' = (pos ∘ succ) h'
  pa  = (pos ∘ succ) a
  pa' = (pos ∘ succ) a'
  pb  = (pos ∘ succ) b
  pb' = (pos ∘ succ) b'

  γ-lemma : (p q r s : ℤ)
          → p ℤ* q ℤ* (r ℤ* s) ＝ p ℤ* r ℤ* (q ℤ* s)
  γ-lemma p q r s =
   p ℤ* q ℤ* (r ℤ* s)   ＝⟨ ℤ*-assoc p q (r ℤ* s)                  ⟩
   p ℤ* (q ℤ* (r ℤ* s)) ＝⟨ ap (p ℤ*_) (ℤ*-assoc q r s ⁻¹)         ⟩
   p ℤ* (q ℤ* r ℤ* s)   ＝⟨ ap (λ - → p ℤ* (- ℤ* s)) (ℤ*-comm q r) ⟩
   p ℤ* (r ℤ* q ℤ* s)   ＝⟨ ap (p ℤ*_) (ℤ*-assoc r q s)            ⟩
   p ℤ* (r ℤ* (q ℤ* s)) ＝⟨ ℤ*-assoc p r (q ℤ* s) ⁻¹               ⟩
   p ℤ* r ℤ* (q ℤ* s)   ∎

  γ₁ : (x , a) ≈ (y , b) → toℚ (x , a) ＝ toℚ (y , b)
  γ₁ e = to-subtype-＝ is-in-lowest-terms-is-prop γ
   where
    I : is-in-lowest-terms (x' , a')
    I = iltℚ (x , a)

    II : is-in-lowest-terms (y' , b')
    II = iltℚ (y , b)

    III : ph ℤ* ph' ℤ* (x' ℤ* pb') ＝ ph ℤ* ph' ℤ* (y' ℤ* pa')
    III = ph ℤ* ph' ℤ* (x' ℤ* pb') ＝⟨ γ-lemma ph ph' x' pb'                  ⟩
          ph ℤ* x' ℤ* (ph' ℤ* pb') ＝⟨ ap (ph ℤ* x' ℤ*_) (dnomrP' (y , b) ⁻¹) ⟩
          ph ℤ* x' ℤ* pb           ＝⟨ ap (_ℤ* pb) (numr (x , a) ⁻¹)          ⟩
          x ℤ* pb                  ＝⟨ e                                      ⟩
          y ℤ* pa                  ＝⟨ ap (_ℤ* pa) (numr (y , b))             ⟩
          ph' ℤ* y' ℤ* pa          ＝⟨ ap (ph' ℤ* y' ℤ*_) (dnomrP' (x , a))   ⟩
          ph' ℤ* y' ℤ* (ph ℤ* pa') ＝⟨ γ-lemma ph' ph y' pa' ⁻¹               ⟩
          ph' ℤ* ph ℤ* (y' ℤ* pa') ＝⟨ ap (_ℤ* (y' ℤ* pa')) (ℤ*-comm ph' ph)  ⟩
          ph ℤ* ph' ℤ* (y' ℤ* pa') ∎

    IV : not-zero (ph ℤ* ph')
    IV iz = non-zero-multiplication ph ph' hnz hnz' piz
     where
      hnz : ph ≠ pos 0
      hnz = pos-succ-not-zero h

      hnz' : ph' ≠ pos 0
      hnz' = pos-succ-not-zero h'

      piz : ph ℤ* ph' ＝ pos 0
      piz = from-is-zero (ph ℤ* ph') iz

    V : x' ℤ* pb' ＝ y' ℤ* pa'
    V = ℤ-mult-left-cancellable (x' ℤ* pb') (y' ℤ* pa') (ph ℤ* ph') IV III

    γ : (x' , a') ＝ (y' , b')
    γ = equiv-with-lowest-terms-is-equal (x' , a') (y' , b') V I II

  γ₂ : toℚ (x , a) ＝ toℚ (y , b) → (x , a) ≈ (y , b)
  γ₂ e = x ℤ* pos (succ b)        ＝⟨ ap (x ℤ*_) (dnomrP' (y , b))           ⟩
         x ℤ* (ph' ℤ* pb')        ＝⟨ ap (_ℤ* (ph' ℤ* pb')) (numr (x , a))   ⟩
         ph ℤ* x' ℤ* (ph' ℤ* pb') ＝⟨ γ-lemma ph x' ph' pb'                  ⟩
         ph ℤ* ph' ℤ* (x' ℤ* pb') ＝⟨ ap (_ℤ* (x' ℤ* pb')) (ℤ*-comm ph ph')  ⟩
         ph' ℤ* ph ℤ* (x' ℤ* pb') ＝⟨ ap (λ - → ph' ℤ* ph ℤ* (- ℤ* pb')) I   ⟩
         ph' ℤ* ph ℤ* (y' ℤ* pb') ＝⟨ ap (λ - → ph' ℤ* ph ℤ* (y' ℤ* -) ) II  ⟩
         ph' ℤ* ph ℤ* (y' ℤ* pa') ＝⟨ γ-lemma ph' y' ph pa' ⁻¹               ⟩
         ph' ℤ* y' ℤ* (ph ℤ* pa') ＝⟨ ap (_ℤ* (ph ℤ* pa')) (numr (y , b) ⁻¹) ⟩
         y ℤ* (ph ℤ* pa')         ＝⟨ ap (y ℤ*_) (dnomrP' (x , a) ⁻¹)        ⟩
         y ℤ* pos (succ a)        ∎
   where
    I : x' ＝ y'
    I = ap (pr₁ ∘ pr₁) e

    II : pb' ＝ pa'
    II = ap (pos ∘ succ ∘ pr₂ ∘ pr₁) (e ⁻¹)

equiv→equality : (p q : 𝔽) → p ≈ q → toℚ p ＝ toℚ q
equiv→equality p q = pr₁ (equiv-equality p q)

equality→equiv : (p q : 𝔽) → toℚ p ＝ toℚ q → p ≈ q
equality→equiv p q = pr₂ (equiv-equality p q)

toℚ-to𝔽 : ((p , α) : ℚ) → (p , α) ＝ toℚ p
toℚ-to𝔽 ((x , a) , α) = to-subtype-＝ is-in-lowest-terms-is-prop γ
 where
  x'  = numℚ (x , a)
  a'  = dnomℚ (x , a)
  h   = hcf𝔽 (x , a)
  pa' = (pos ∘ succ) a'
  pa  = (pos ∘ succ) a
  ph  = (pos ∘ succ) h

  I : coprime (abs x) (succ a)
  I = coprime'-to-coprime (abs x) (succ a) α

  II : (x , a) ≈ (x' , a')
  II = x ℤ* pa'          ＝⟨ ap (_ℤ* pa') (numr (x , a))      ⟩
       ph ℤ* x' ℤ* pa'   ＝⟨ ap (_ℤ* pa') (ℤ*-comm ph x')     ⟩
       x' ℤ* ph ℤ* pa'   ＝⟨ ℤ*-assoc x' ph pa'               ⟩
       x' ℤ* (ph ℤ* pa') ＝⟨ ap (x' ℤ*_) (dnomrP' (x , a) ⁻¹) ⟩
       x' ℤ* pa          ∎

  γ : (x , a) ＝ (x' , a')
  γ = equiv-with-lowest-terms-is-equal (x , a) (x' , a') II α (iltℚ (x , a))

ℚ-＝ : ((p , α) (q , β) : ℚ) → p ≈ q → (p , α) ＝ (q , β)
ℚ-＝ (p , α) (q , β) e = to-subtype-＝ is-in-lowest-terms-is-prop I
 where
  I : p ＝ q
  I = equiv-with-lowest-terms-is-equal p q e α β

≈-toℚ : (p : 𝔽) → p ≈ to𝔽 (toℚ p)
≈-toℚ p = equality→equiv p p' (toℚ-to𝔽 (toℚ p))
 where
  p' = to𝔽 (toℚ p)

q-has-qn : (q : ℚ) → Σ q' ꞉ 𝔽 , q ＝ toℚ q'
q-has-qn (q , α) =  q , toℚ-to𝔽 (q , α)

ℚ-zero-not-one :  ¬ (0ℚ ＝ 1ℚ)
ℚ-zero-not-one e = positive-not-zero 0 (pos-lc γ ⁻¹)
 where
  I : toℚ (pos 0 , 0) ＝ toℚ (pos 1 , 0) → (pos 0 , 0) ≈ (pos 1 , 0)
  I = equality→equiv (pos 0 , 0) (pos 1 , 0)

  γ : pos 0 ＝ pos 1
  γ = pos 0          ＝⟨ refl ⟩
      pos 0 ℤ* pos 1 ＝⟨ I e  ⟩
      pos 1 ℤ* pos 1 ＝⟨ refl ⟩
      pos 1          ∎

ℚ-positive-not-zero : (x a : ℕ) → ¬ (toℚ (pos (succ x) , a) ＝ 0ℚ)
ℚ-positive-not-zero x a e = pos-succ-not-zero x γ
 where
  I : (pos (succ x) , a) ≈ (pos 0 , 0)
  I = equality→equiv (pos (succ x) , a) (pos 0 , 0) e

  γ : pos (succ x) ＝ pos 0
  γ = pos (succ x)            ＝⟨ by-definition                    ⟩
      pos (succ x) ℤ* (pos 1) ＝⟨ I                                ⟩
      pos 0 ℤ* pos (succ a)   ＝⟨ ℤ-zero-left-base (pos (succ a))  ⟩
      pos 0                   ∎

ℚ-negative-not-zero : (x a : ℕ) → ¬ (toℚ (negsucc x , a) ＝ 0ℚ)
ℚ-negative-not-zero x a e = negsucc-not-zero x γ
 where
  I : (negsucc x , a) ≈ (pos 0 , 0)
  I = equality→equiv (negsucc x , a) (pos 0 , 0) e

  γ : negsucc x ＝ pos 0
  γ = negsucc x             ＝⟨ refl                            ⟩
      negsucc x ℤ* pos 1    ＝⟨ I                               ⟩
      pos 0 ℤ* pos (succ a) ＝⟨ ℤ-zero-left-base (pos (succ a)) ⟩
      pos 0                 ∎

numerator-zero-is-zero : (((x , a) , p) : ℚ) → x ＝ pos 0 → (x , a) , p ＝ 0ℚ
numerator-zero-is-zero ((negsucc x , a) , p) e = 𝟘-elim (negsucc-not-pos e)
numerator-zero-is-zero ((pos (succ x) , a) , p) e = 𝟘-elim γ
 where
  γ : 𝟘
  γ = positive-not-zero x (pos-lc e)
numerator-zero-is-zero ((pos 0 , a) , p) e = γ
 where
  I : (pos 0 , a) ≈ (pos 0 , 0)
  I = pos 0 ℤ* pos 1        ＝⟨ refl                               ⟩
      pos 0                 ＝⟨ ℤ-zero-left-base (pos (succ a)) ⁻¹ ⟩
      pos 0 ℤ* pos (succ a) ∎

  γ : (pos 0 , a) , p ＝ 0ℚ
  γ = (pos 0 , a) , p ＝⟨ toℚ-to𝔽 ((pos 0 , a) , p)                ⟩
      toℚ (pos 0 , a) ＝⟨ equiv→equality (pos 0 , a) (pos 0 , 0) I ⟩
      toℚ (pos 0 , 0) ＝⟨ refl                                     ⟩
      0ℚ ∎

instance
 canonical-map-𝔽-to-ℚ : Canonical-Map 𝔽 ℚ
 ι {{canonical-map-𝔽-to-ℚ}} = toℚ

ℤ-to-ℚ : ℤ → ℚ
ℤ-to-ℚ z = ι (ι z)

instance
 canonical-map-ℤ-to-ℚ : Canonical-Map ℤ ℚ
 ι {{canonical-map-ℤ-to-ℚ}} = ℤ-to-ℚ

ℕ-to-ℚ : ℕ → ℚ
ℕ-to-ℚ n = ι {{ canonical-map-ℤ-to-ℚ }} (ι n)

instance
 canonical-map-ℕ-to-ℚ : Canonical-Map ℕ ℚ
 ι {{canonical-map-ℕ-to-ℚ}} = ℕ-to-ℚ

\end{code}
