Type
Andrew Sneap, November 2020 - March 2021
In this file I define rational numbers.
{-# 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.SigmaDiscrete
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-ℚ