Andrew Sneap, November 2021
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan renaming (_+_ to _∔_)
open import Naturals.Addition renaming (_+_ to _ℕ+_)
open import Naturals.Properties
open import UF.Base hiding (_≈_)
open import Integers.Type hiding (abs)
open import Integers.Abs
open import Integers.Addition renaming (_+_ to _ℤ+_)
open import Integers.Multiplication renaming (_*_ to _ℤ*_)
open import Integers.Negation renaming (-_ to ℤ-_)
open import Rationals.Fractions
open import Naturals.Multiplication renaming (_*_ to _ℕ*_)
module Rationals.FractionsOperations where
\end{code}
The denom-setup function is useful to manipulate denominators into an easier to work with form.
\begin{code}
denom-setup : (a b : ℕ) → pos (succ (pred (succ a ℕ* succ b))) ＝ pos (succ a) ℤ* pos (succ b)
denom-setup a b = pos (succ (pred (succ a ℕ* succ b))) ＝⟨ i ⟩
pos (succ a ℕ* succ b) ＝⟨ ii ⟩
pos (succ a) ℤ* pos (succ b) ∎
where
i = ap pos (succ-pred-multiplication a b ⁻¹)
ii = pos-multiplication-equiv-to-ℕ (succ a) (succ b) ⁻¹
-_ : 𝔽 → 𝔽
-_ (x , a) = ℤ- x , a
_+_ : 𝔽 → 𝔽 → 𝔽
(x , y) + (x' , y')
= x ℤ* pos (succ y') ℤ+ x' ℤ* pos (succ y) , pred (succ y ℕ* succ y')
infixl 33 _+_
𝔽-zero-right-neutral : (q : 𝔽) → q + (pos 0 , 0) ＝ q
𝔽-zero-right-neutral (x , a)
= (x , a) + (pos 0 , 0) ＝⟨ refl ⟩
x ℤ+ (pos 0 ℤ* pos (succ a)) , a ＝⟨ i ⟩
x ℤ+ pos 0 , a ＝⟨ refl ⟩
x , a ∎
where
i = ap (λ - → x ℤ+ - , a) (ℤ*-comm (pos 0) (pos (succ a)))
𝔽+-comm : (p q : 𝔽) → p + q ＝ q + p
𝔽+-comm (x , a) (y , b) = ap₂ _,_ I II
where
I : x ℤ* pos (succ b) ℤ+ y ℤ* pos (succ a)
＝ y ℤ* pos (succ a) ℤ+ x ℤ* pos (succ b)
I = ℤ+-comm (x ℤ* pos (succ b)) (y ℤ* (pos (succ a)))
II : pred (succ a ℕ* succ b) ＝ pred (succ b ℕ* succ a)
II = ap pred (mult-commutativity (succ a) (succ b))
𝔽+-assoc : (a b c : 𝔽) → a + b + c ＝ a + (b + c)
𝔽+-assoc (x , a) (y , b) (z , c) = ap₂ _,_ I II
where
left : 𝔽
left = (x , a) + (y , b)
right : 𝔽
right = (y , b) + (z , c)
α δ : ℤ
α = pr₁ left
δ = pr₁ right
β γ : ℕ
β = pr₂ left
γ = pr₂ right
a' = pos (succ a)
b' = pos (succ b)
c' = pos (succ c)
I : α ℤ* c' ℤ+ z ℤ* pos (succ (pred (succ a ℕ* succ b)))
＝ x ℤ* pos (succ (pred (succ b ℕ* succ c))) ℤ+ δ ℤ* a'
I = α ℤ* c' ℤ+ z ℤ* pos (succ (pred (succ a ℕ* succ b))) ＝⟨ i ⟩
(x ℤ* b' ℤ+ y ℤ* a') ℤ* c' ℤ+ z ℤ* pos (succ a ℕ* succ b) ＝⟨ ii ⟩
(x ℤ* b' ℤ+ y ℤ* a') ℤ* c' ℤ+ z ℤ* (a' ℤ* b') ＝⟨ iii ⟩
x ℤ* b' ℤ* c' ℤ+ y ℤ* a' ℤ* c' ℤ+ z ℤ* (b' ℤ* a') ＝⟨ iv ⟩
x ℤ* b' ℤ* c' ℤ+ (y ℤ* a' ℤ* c' ℤ+ z ℤ* (b' ℤ* a')) ＝⟨ v ⟩
x ℤ* (b' ℤ* c') ℤ+ (y ℤ* c' ℤ* a' ℤ+ z ℤ* b' ℤ* a') ＝⟨ vi ⟩
x ℤ* (b' ℤ* c') ℤ+ (y ℤ* c' ℤ+ z ℤ* b') ℤ* a' ＝⟨ vii ⟩
x ℤ* pos (succ b ℕ* succ c) ℤ+ (y ℤ* c' ℤ+ z ℤ* b') ℤ* a' ＝⟨ viii ⟩
x ℤ* pos (succ (pred (succ b ℕ* succ c))) ℤ+ δ ℤ* a' ∎
where
iₐₚ : succ (pred (succ a ℕ* succ b)) ＝ succ a ℕ* succ b
iₐₚ = succ-pred-multiplication a b ⁻¹
iiₐₚ : pos (succ a ℕ* succ b) ＝ a' ℤ* b'
iiₐₚ = pos-multiplication-equiv-to-ℕ (succ a) (succ b) ⁻¹
iiiₐₚ : z ℤ* (a' ℤ* b') ＝ z ℤ* (b' ℤ* a')
iiiₐₚ = ap (z ℤ*_) (ℤ*-comm a' b')
vₐₚ₁ : y ℤ* a' ℤ* c' ＝ y ℤ* c' ℤ* a'
vₐₚ₁ = ℤ-mult-rearrangement y a' c'
vₐₚ₂ : z ℤ* (b' ℤ* a') ＝ z ℤ* b' ℤ* a'
vₐₚ₂ = ℤ*-assoc z b' a' ⁻¹
viₐₚ : y ℤ* c' ℤ* a' ℤ+ z ℤ* b' ℤ* a' ＝ (y ℤ* c' ℤ+ z ℤ* b') ℤ* a'
viₐₚ = distributivity-mult-over-ℤ (y ℤ* c') (z ℤ* b') a' ⁻¹
viiₐₚ : b' ℤ* c' ＝ pos (succ b ℕ* succ c)
viiₐₚ = pos-multiplication-equiv-to-ℕ (succ b) (succ c)
viiiₐₚ : succ b ℕ* succ c ＝ succ (pred (succ b ℕ* succ c))
viiiₐₚ = succ-pred-multiplication b c
i = ap (λ - → α ℤ* c' ℤ+ z ℤ* pos -) iₐₚ
ii = ap (λ - → (x ℤ* b' ℤ+ y ℤ* a') ℤ* c' ℤ+ z ℤ* -) iiₐₚ
iii = ap₂ _ℤ+_ (distributivity-mult-over-ℤ (x ℤ* b') (y ℤ* a') c') iiiₐₚ
iv = ℤ+-assoc (x ℤ* b' ℤ* c') (y ℤ* a' ℤ* c') (z ℤ* (b' ℤ* a'))
v = ap₂ _ℤ+_ (ℤ*-assoc x b' c') (ap₂ _ℤ+_ vₐₚ₁ vₐₚ₂)
vi = ap (λ - → x ℤ* (b' ℤ* c') ℤ+ - ) viₐₚ
vii = ap (λ - → x ℤ* - ℤ+ (y ℤ* c' ℤ+ z ℤ* b') ℤ* a') viiₐₚ
viii = ap (λ - → x ℤ* pos - ℤ+ δ ℤ* a') viiiₐₚ
II : pred (succ (pred (succ a ℕ* (succ b))) ℕ* succ c)
＝ pred (succ a ℕ* succ (pred (succ b ℕ+ succ b ℕ* c)))
II = pred (succ (pred (succ a ℕ* succ b)) ℕ* succ c) ＝⟨ i ⟩
pred (succ a ℕ* succ b ℕ* succ c) ＝⟨ ii ⟩
pred (succ a ℕ* (succ b ℕ* succ c)) ＝⟨ iii ⟩
pred (succ a ℕ* succ (pred (succ b ℕ+ succ b ℕ* c))) ∎
where
i = ap (λ - → pred (- ℕ* succ c)) (succ-pred-multiplication a b ⁻¹)
ii = ap pred (mult-associativity (succ a) (succ b) (succ c))
iii = ap (λ - → pred (succ a ℕ* -)) (succ-pred-multiplication b c)
≈-addition : (p q r : 𝔽) → p ≈ q → (p + r) ≈ (q + r)
≈-addition (x , a) (y , b) (z , c) e₁ = III
where
I : pos (succ (pred (succ b ℕ* succ c))) ＝ pos (succ b) ℤ* pos (succ c)
I = denom-setup b c
II : pos (succ a) ℤ* pos (succ c) ＝ pos (succ (pred (succ a ℕ* succ c)))
II = denom-setup a c ⁻¹
a' b' c' : ℤ
a' = pos (succ a)
b' = pos (succ b)
c' = pos (succ c)
III : (x , a) + (z , c) ≈ (y , b) + (z , c)
III = (x ℤ* c' ℤ+ (z ℤ* a')) ℤ* pos (succ (pred (succ b ℕ* succ c))) ＝⟨ i ⟩
(x ℤ* c' ℤ+ z ℤ* a') ℤ* (b' ℤ* c') ＝⟨ ii ⟩
x ℤ* c' ℤ* (b' ℤ* c') ℤ+ z ℤ* a' ℤ* (b' ℤ* c') ＝⟨ iii ⟩
x ℤ* (b' ℤ* c') ℤ* c' ℤ+ z ℤ* (b' ℤ* c') ℤ* a' ＝⟨ iv ⟩
x ℤ* b' ℤ* c' ℤ* c' ℤ+ z ℤ* b' ℤ* c' ℤ* a' ＝⟨ v ⟩
y ℤ* a' ℤ* c' ℤ* c' ℤ+ z ℤ* b' ℤ* (c' ℤ* a') ＝⟨ vi ⟩
y ℤ* c' ℤ* a' ℤ* c' ℤ+ z ℤ* b' ℤ* (a' ℤ* c') ＝⟨ vii ⟩
y ℤ* c' ℤ* (a' ℤ* c') ℤ+ z ℤ* b' ℤ* (a' ℤ* c') ＝⟨ viii ⟩
(y ℤ* c' ℤ+ z ℤ* b') ℤ* (a' ℤ* c') ＝⟨ ix ⟩
(y ℤ* c' ℤ+ (z ℤ* b')) ℤ* pos (succ (pred (succ a ℕ* succ c))) ∎
where
iiiₐₚ = ℤ-mult-rearrangement z a' (b' ℤ* c')
ivₐₚ = ap (_ℤ* a') (ℤ*-assoc z b' c' ⁻¹)
viₐₚ = ap (λ - → z ℤ* b' ℤ* -) (ℤ*-comm c' a')
i = ap (λ - → (x ℤ* c' ℤ+ (z ℤ* a')) ℤ* -) I
ii = distributivity-mult-over-ℤ (x ℤ* c') (z ℤ* a') (b' ℤ* c')
iii = ap₂ _ℤ+_ (ℤ-mult-rearrangement x c' (b' ℤ* c')) iiiₐₚ
iv = ap₂ _ℤ+_ (ap (_ℤ* c') (ℤ*-assoc x b' c' ⁻¹)) ivₐₚ
v = ap₂ _ℤ+_ (ap (λ - → - ℤ* c' ℤ* c') e₁) (ℤ*-assoc (z ℤ* b') c' a')
vi = ap₂ _ℤ+_ (ap (_ℤ* c') (ℤ-mult-rearrangement y a' c')) viₐₚ
vii = ap (_ℤ+ z ℤ* b' ℤ* (a' ℤ* c')) (ℤ*-assoc (y ℤ* c') a' c')
viii = distributivity-mult-over-ℤ (y ℤ* c') (z ℤ* b') (a' ℤ* c') ⁻¹
ix = ap (λ - → (y ℤ* c' ℤ+ (z ℤ* b')) ℤ* -) II
_*_ : 𝔽 → 𝔽 → 𝔽
(x , y) * (x' , y') = x ℤ* x' , pred (succ y ℕ* succ y')
infixl 34 _*_
≈-over-* : (p q r : 𝔽) → p ≈ q → (p * r) ≈ (q * r)
≈-over-* (x , a) (y , b) (z , c) e = I
where
a' b' c' : ℤ
a' = pos (succ a)
b' = pos (succ b)
c' = pos (succ c)
I : x ℤ* z ℤ* pos (succ (pred (succ b ℕ* succ c)))
＝ y ℤ* z ℤ* pos (succ (pred (succ a ℕ* succ c)))
I = x ℤ* z ℤ* pos (succ (pred (succ b ℕ* succ c))) ＝⟨ i ⟩
x ℤ* z ℤ* (b' ℤ* c') ＝⟨ ii ⟩
x ℤ* z ℤ* b' ℤ* c' ＝⟨ iii ⟩
x ℤ* b' ℤ* z ℤ* c' ＝⟨ iv ⟩
y ℤ* a' ℤ* z ℤ* c' ＝⟨ v ⟩
y ℤ* (a' ℤ* z) ℤ* c' ＝⟨ vi ⟩
y ℤ* (z ℤ* a') ℤ* c' ＝⟨ vii ⟩
y ℤ* z ℤ* a' ℤ* c' ＝⟨ viii ⟩
y ℤ* z ℤ* (a' ℤ* c') ＝⟨ ix ⟩
y ℤ* z ℤ* pos (succ (pred (succ a ℕ* succ c))) ∎
where
i = ap (λ - → x ℤ* z ℤ* -) (denom-setup b c)
ii = ℤ*-assoc (x ℤ* z) b' c' ⁻¹
iii = ap (_ℤ* c') (ℤ-mult-rearrangement x z b')
iv = ap (λ - → - ℤ* z ℤ* c') e
v = ap (_ℤ* c') (ℤ*-assoc y a' z )
vi = ap (λ - → y ℤ* - ℤ* c') (ℤ*-comm a' z)
vii = ap (_ℤ* c') (ℤ*-assoc y z a' ⁻¹)
viii = ℤ*-assoc (y ℤ* z) a' c'
ix = ap (λ - → (y ℤ* z ℤ* -)) (denom-setup a c ⁻¹)
1/3+1/3≈2/3 : (pos 1 , 2) + (pos 1 , 2) ≈ (pos 2 , 2)
1/3+1/3≈2/3 = refl
1/3+2/3≈1 : (pos 1 , 2) + (pos 2 , 2) ≈ (pos 1 , 0)
1/3+2/3≈1 = refl
𝔽-mult-left-id : (q : 𝔽) → (pos 1 , 0) * q ＝ q
𝔽-mult-left-id (x , a) = to-×-＝ γ₁ γ₂
where
γ₁ : pos 1 ℤ* x ＝ x
γ₁ = ℤ-mult-left-id x
γ₂ : pred (1 ℕ* succ a) ＝ a
γ₂ = ap pred (mult-commutativity 1 (succ a))
𝔽-zero-left-is-zero : (q : 𝔽) → (pos 0 , 0) * q ≈ (pos 0 , 0)
𝔽-zero-left-is-zero (x , a)
= pos 0 ℤ* x ℤ* pos 1 ＝⟨ i ⟩
pos 0 ℤ* (x ℤ* pos 1) ＝⟨ ii ⟩
pos 0 ＝⟨ iii ⟩
pos 0 ℤ* pos (succ (pred (1 ℕ* succ a))) ∎
where
i = ℤ*-assoc (pos 0) x (pos 1)
ii = ℤ-zero-left-base (x ℤ* pos 1)
iii = ℤ-zero-left-base (pos (succ (pred (1 ℕ* succ a)))) ⁻¹
𝔽*-comm : (p q : 𝔽) → p * q ＝ q * p
𝔽*-comm (x , a) (y , b) = ap₂ _,_ I II
where
I : x ℤ* y ＝ y ℤ* x
I = ℤ*-comm x y
II : pred (succ a ℕ* succ b) ＝ pred (succ b ℕ* succ a)
II = ap pred (mult-commutativity (succ a) (succ b))
𝔽*-assoc : (p q r : 𝔽) → p * q * r ＝ p * (q * r)
𝔽*-assoc (x , a) (y , b) (z , c) = ap₂ _,_ I II
where
I : x ℤ* y ℤ* z ＝ x ℤ* (y ℤ* z)
I = ℤ*-assoc x y z
a' b' c' : ℕ
a' = succ a
b' = succ b
c' = succ c
II : pred (succ (pred (a' ℕ* b')) ℕ* c') ＝ pred (a' ℕ* succ (pred (b' ℕ* c')))
II = pred (succ (pred (a' ℕ* b')) ℕ* c') ＝⟨ i ⟩
pred (a' ℕ* b' ℕ* c') ＝⟨ ii ⟩
pred (a' ℕ* (b' ℕ* c')) ＝⟨ iii ⟩
pred (a' ℕ* succ (pred (b' ℕ* c'))) ∎
where
i = ap (λ - → pred (- ℕ* c')) (succ-pred-multiplication a b ⁻¹)
ii = ap pred (mult-associativity a' b' c')
iii = ap (λ - → pred (a' ℕ* -)) (succ-pred-multiplication b c)
𝔽-dist : (p q r : 𝔽) → p * (q + r) ≈ p * q + p * r
𝔽-dist (x , a) (y , b) (z , c) = I
where
a' b' c' : ℕ
a' = succ a
b' = succ b
c' = succ c
a'' b'' c'' k l : ℤ
a'' = pos a'
b'' = pos b'
c'' = pos c'
k = pos (succ (pred (a' ℕ* c')))
l = pos (succ (pred (a' ℕ* b')))
I-lemma : (x y p q : ℤ) → x ℤ* y ℤ* (p ℤ* q) ＝ x ℤ* p ℤ* (y ℤ* q)
I-lemma x y p q = x ℤ* y ℤ* (p ℤ* q) ＝⟨ ℤ*-assoc (x ℤ* y) p q ⁻¹ ⟩
x ℤ* y ℤ* p ℤ* q ＝⟨ ap (_ℤ* q) (ℤ*-assoc x y p ) ⟩
x ℤ* (y ℤ* p) ℤ* q ＝⟨ ap (λ - → x ℤ* - ℤ* q) (ℤ*-comm y p) ⟩
x ℤ* (p ℤ* y) ℤ* q ＝⟨ ap (_ℤ* q) (ℤ*-assoc x p y ⁻¹) ⟩
x ℤ* p ℤ* y ℤ* q ＝⟨ ℤ*-assoc (x ℤ* p) y q ⟩
x ℤ* p ℤ* (y ℤ* q) ∎
I : _ ＝ _
I = x ℤ* (y ℤ* c'' ℤ+ z ℤ* b'') ℤ* pos (succ (pred (succ (pred (a' ℕ* b')) ℕ* (succ (pred (a' ℕ* c')))))) ＝⟨ i ⟩
x ℤ* (y ℤ* c'' ℤ+ z ℤ* b'') ℤ* (l ℤ* k) ＝⟨ ii ⟩
x ℤ* (y ℤ* c'' ℤ+ z ℤ* b'') ℤ* (pos (a' ℕ* b') ℤ* pos (a' ℕ* c')) ＝⟨ iii ⟩
x ℤ* (y ℤ* c'' ℤ+ z ℤ* b'') ℤ* (a'' ℤ* b'' ℤ* (a'' ℤ* c'')) ＝⟨ iv ⟩
x ℤ* (y ℤ* c'' ℤ+ z ℤ* b'') ℤ* (a'' ℤ* (b'' ℤ* (a'' ℤ* c''))) ＝⟨ v ⟩
x ℤ* (y ℤ* c'' ℤ+ z ℤ* b'') ℤ* a'' ℤ* (b'' ℤ* (a'' ℤ* c'')) ＝⟨ vi ⟩
x ℤ* a'' ℤ* (y ℤ* c'' ℤ+ (z ℤ* b'')) ℤ* (a'' ℤ* (b'' ℤ* c'')) ＝⟨ vii ⟩
(x ℤ* a'' ℤ* (y ℤ* c'') ℤ+ x ℤ* a'' ℤ* (z ℤ* b'')) ℤ* (a'' ℤ* (pos (b' ℕ* c'))) ＝⟨ viii ⟩
(x ℤ* y ℤ* (a'' ℤ* c'') ℤ+ x ℤ* z ℤ* (a'' ℤ* b'')) ℤ* (a'' ℤ* (pos (b' ℕ* c'))) ＝⟨ ix ⟩
(x ℤ* y ℤ* k ℤ+ (x ℤ* z ℤ* l)) ℤ* (a'' ℤ* (pos (b' ℕ* c'))) ＝⟨ xi ⟩
(x ℤ* y ℤ* k ℤ+ (x ℤ* z ℤ* l)) ℤ* pos (a' ℕ* (b' ℕ* c')) ＝⟨ xii ⟩
(x ℤ* y ℤ* k ℤ+ (x ℤ* z ℤ* l)) ℤ* pos (a' ℕ* succ (pred (b' ℕ* c'))) ＝⟨ xiii ⟩
(x ℤ* y ℤ* k ℤ+ (x ℤ* z ℤ* l)) ℤ* pos (succ (pred (a' ℕ* succ (pred (b' ℕ* c'))))) ∎
where
i = ap (λ β → x ℤ* (y ℤ* c'' ℤ+ (z ℤ* b'')) ℤ* β ) (denom-setup (pred (a' ℕ* b')) (pred (a' ℕ* c')))
ii = ap₂ (λ α β → x ℤ* (y ℤ* c'' ℤ+ (z ℤ* b'')) ℤ* (pos α ℤ* pos β)) (succ-pred-multiplication a b ⁻¹) (succ-pred-multiplication a c ⁻¹)
iii = ap₂ (λ α β → x ℤ* (y ℤ* c'' ℤ+ (z ℤ* b'')) ℤ* (α ℤ* β) ) (pos-multiplication-equiv-to-ℕ a' b' ⁻¹) (pos-multiplication-equiv-to-ℕ a' c' ⁻¹)
iv = ap (λ α → x ℤ* (y ℤ* c'' ℤ+ (z ℤ* b'')) ℤ* α ) (ℤ*-assoc a'' b'' ( a'' ℤ* c'') )
v = ℤ*-assoc (x ℤ* ( y ℤ* c'' ℤ+ (z ℤ* b'') )) a'' ( b'' ℤ* (a'' ℤ* c'')) ⁻¹
vi = ap₂ (λ α β → α ℤ* β) (ℤ-mult-rearrangement x ( y ℤ* c'' ℤ+ (z ℤ* b'')) a'') (ℤ-mult-rearrangement''' b'' a'' c'')
vii = ap₂ (λ α β → α ℤ* (a'' ℤ* β)) (distributivity-mult-over-ℤ' (y ℤ* c'') (z ℤ* b'') (x ℤ* a'')) (pos-multiplication-equiv-to-ℕ b' c')
viii = ap₂ (λ α β → (α ℤ+ β) ℤ* ((a'' ℤ* (pos (b' ℕ* c'))))) (I-lemma x a'' y c'') (I-lemma x a'' z b'')
ix = ap₂ (λ α β → (x ℤ* y ℤ* α ℤ+ x ℤ* z ℤ* β) ℤ* ((a'' ℤ* (pos (b' ℕ* c'))))) (denom-setup a c ⁻¹) (denom-setup a b ⁻¹)
xi = ap (λ α → (x ℤ* y ℤ* k ℤ+ (x ℤ* z ℤ* l)) ℤ* α) (pos-multiplication-equiv-to-ℕ a' (b' ℕ* c'))
xii = ap (λ α → (x ℤ* y ℤ* k ℤ+ (x ℤ* z ℤ* l)) ℤ* (pos (a' ℕ* α))) (succ-pred-multiplication b c)
xiii = ap (λ α → (x ℤ* y ℤ* k ℤ+ (x ℤ* z ℤ* l)) ℤ* pos α) (succ-pred-multiplication a (pred (b' ℕ* c')))
abs : 𝔽 → 𝔽
abs (x , a) = absℤ x , a
𝔽-abs-0 : pos 0 , 0 ＝ abs (pos 0 , 0)
𝔽-abs-0 = by-definition
𝔽-abs-neg-equals-pos : (q : 𝔽) → abs q ≈ abs (- q)
𝔽-abs-neg-equals-pos (x , a) = ap (_ℤ* (pos (succ a))) (absℤ-removes-neg-sign x)
𝔽-subtraction-dist-over-mult : (p q : 𝔽) → (- p) * q ≈ (- (p * q))
𝔽-subtraction-dist-over-mult (x , a) (y , b) = γ
where
I : (ℤ- x) ℤ* y ＝ ℤ- (x ℤ* y)
I = negation-dist-over-mult' x y
γ : _
γ = ap (_ℤ* pos (succ (pred (succ a ℕ* succ b)))) I
𝔽-minus-dist : ((x , a) (y , b) : 𝔽)
→ (ℤ- x , a) + (ℤ- y , b) ≈ (- ((x , a) + (y , b)))
𝔽-minus-dist (x , a) (y , b) = γ
where
pa = (pos ∘ succ) a
pb = (pos ∘ succ) b
γ' : (ℤ- x) ℤ* pb ℤ+ (ℤ- y) ℤ* pa ＝ ℤ- (x ℤ* pb ℤ+ y ℤ* pa)
γ' = (ℤ- x) ℤ* pb ℤ+ (ℤ- y) ℤ* pa ＝⟨ i ⟩
(ℤ- x ℤ* pb) ℤ+ (ℤ- y) ℤ* pa ＝⟨ ii ⟩
(ℤ- x ℤ* pb) ℤ+ (ℤ- y ℤ* pa) ＝⟨ iii ⟩
ℤ- (x ℤ* pb ℤ+ y ℤ* pa) ∎
where
i = ap (_ℤ+ (ℤ- y) ℤ* pa) (negation-dist-over-mult' x pb)
ii = ap ((ℤ- x ℤ* pb) ℤ+_) (negation-dist-over-mult' y pa)
iii = negation-dist (x ℤ* pb) (y ℤ* pa)
γ : ((ℤ- x , a) + (ℤ- y , b)) ≈ (- ((x , a) + (y , b)))
γ = ap (_ℤ* pos (succ (pred (succ a ℕ* succ b)))) γ'
𝔽+-inverse : ((x , a) : 𝔽) → ((ℤ- x , a) + (x , a)) ≈ (pos 0 , 0)
𝔽+-inverse (x , a) = γ
where
pa = (pos ∘ succ) a
γ : ((ℤ- x , a) + (x , a)) ≈ (pos 0 , 0)
γ = ((ℤ- x) ℤ* pa ℤ+ x ℤ* pa) ℤ* pos 1 ＝⟨ i ⟩
((ℤ- x) ℤ* pa ℤ+ x ℤ* pa) ＝⟨ ii ⟩
((ℤ- x) ℤ+ x) ℤ* pa ＝⟨ iii ⟩
(x ℤ+ (ℤ- x)) ℤ* pa ＝⟨ iv ⟩
pos 0 ℤ* pa ＝⟨ v ⟩
pos 0 ＝⟨ vi ⟩
pos 0 ℤ* pos (succ (pred (succ a ℕ* succ a))) ∎
where
i = ℤ-mult-right-id ((ℤ- x) ℤ* pa ℤ+ (x ℤ* pa))
ii = distributivity-mult-over-ℤ (ℤ- x) x pa ⁻¹
iii = ap (_ℤ* pa) (ℤ+-comm (ℤ- x) x)
iv = ap (_ℤ* pa) (ℤ-sum-of-inverse-is-zero x)
v = ℤ-zero-left-base pa
vi = ℤ-zero-left-base (pos (succ (pred (succ a ℕ* succ a)))) ⁻¹
𝔽+-inverse' : ((x , a) : 𝔽) → ((x , a) + (ℤ- x , a)) ≈ (pos 0 , 0)
𝔽+-inverse' (x , a) = γ
where
I : (x , a) + (ℤ- x , a) ＝ (ℤ- x , a) + (x , a)
I = 𝔽+-comm (x , a) (ℤ- x , a)
II : ((x , a) + (ℤ- x , a)) ≈ ((x , a) + (ℤ- x , a))
II = ≈-refl ((x , a) + (ℤ- x , a))
III : ((x , a) + (ℤ- x , a)) ≈ ((ℤ- x , a) + (x , a))
III = transport (((x , a) + (ℤ- x , a)) ≈_) I II
IV : ((ℤ- x , a) + (x , a)) ≈ (pos 0 , 0)
IV = 𝔽+-inverse (x , a)
γ : ((x , a) + (ℤ- x , a)) ≈ (pos 0 , 0)
γ = ≈-trans ((x , a) + (ℤ- x , a)) ((ℤ- x , a) + (x , a)) (pos 0 , 0) III IV
𝔽-add-same-denom : ((x , a) (y , a) : 𝔽) → (((x , a) + (y , a)) ≈ (x ℤ+ y , a))
𝔽-add-same-denom (x , a) (y , b) = γ
where
γ : _
γ = (x ℤ* pos (succ b) ℤ+ y ℤ* pos (succ b)) ℤ* pos (succ b) ＝⟨ i ⟩
(x ℤ+ y) ℤ* pos (succ b) ℤ* pos (succ b) ＝⟨ ii ⟩
(x ℤ+ y) ℤ* (pos (succ b) ℤ* pos (succ b)) ＝⟨ iii ⟩
(x ℤ+ y) ℤ* pos (succ (pred (succ b ℕ* succ b))) ∎
where
i = ap (_ℤ* pos (succ b)) (distributivity-mult-over-ℤ x y (pos (succ b)) ⁻¹)
ii = ℤ*-assoc (x ℤ+ y ) (pos (succ b)) (pos (succ b))
iii = ap ((x ℤ+ y) ℤ*_) (denom-setup b b ⁻¹)
\end{code}