Addition on integer fractions
module elementary-number-theory.addition-integer-fractions where
Imports
open import elementary-number-theory.addition-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.multiplication-integers open import foundation.dependent-pair-types open import foundation.identity-types
Idea
We introduce addition on integer fractions and derive its basic properties. Note that the properties only hold up to fraction similarity.
Definition
add-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ pr1 (add-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos)) = (m *ℤ n') +ℤ (m' *ℤ n) pr1 (pr2 (add-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) = n *ℤ n' pr2 (pr2 (add-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) = is-positive-mul-ℤ n-pos n'-pos add-fraction-ℤ' : fraction-ℤ → fraction-ℤ → fraction-ℤ add-fraction-ℤ' x y = add-fraction-ℤ y x infix 30 _+fraction-ℤ_ _+fraction-ℤ_ = add-fraction-ℤ ap-add-fraction-ℤ : {x y x' y' : fraction-ℤ} → x ＝ x' → y ＝ y' → x +fraction-ℤ y ＝ x' +fraction-ℤ y' ap-add-fraction-ℤ p q = ap-binary add-fraction-ℤ p q
Properties
Addition respects the similarity relation
sim-fraction-add-fraction-ℤ : {x x' y y' : fraction-ℤ} → sim-fraction-ℤ x x' → sim-fraction-ℤ y y' → sim-fraction-ℤ (x +fraction-ℤ y) (x' +fraction-ℤ y') sim-fraction-add-fraction-ℤ {(nx , dx , dxp)} {(nx' , dx' , dx'p)} {(ny , dy , dyp)} {(ny' , dy' , dy'p)} p q = equational-reasoning ((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ (dx' *ℤ dy') ＝ ((nx *ℤ dy) *ℤ (dx' *ℤ dy')) +ℤ ((ny *ℤ dx) *ℤ (dx' *ℤ dy')) by right-distributive-mul-add-ℤ (nx *ℤ dy) (ny *ℤ dx) (dx' *ℤ dy') ＝ ((dy *ℤ nx) *ℤ (dx' *ℤ dy')) +ℤ ((dx *ℤ ny) *ℤ (dy' *ℤ dx')) by ap-add-ℤ (ap-mul-ℤ (commutative-mul-ℤ nx dy) refl) (ap-mul-ℤ (commutative-mul-ℤ ny dx) (commutative-mul-ℤ dx' dy')) ＝ (((dy *ℤ nx) *ℤ dx') *ℤ dy') +ℤ (((dx *ℤ ny) *ℤ dy') *ℤ dx') by ap-add-ℤ (inv (associative-mul-ℤ (dy *ℤ nx) dx' dy')) (inv (associative-mul-ℤ (dx *ℤ ny) dy' dx')) ＝ ((dy *ℤ (nx *ℤ dx')) *ℤ dy') +ℤ ((dx *ℤ (ny *ℤ dy')) *ℤ dx') by ap-add-ℤ (ap-mul-ℤ (associative-mul-ℤ dy nx dx') refl) (ap-mul-ℤ (associative-mul-ℤ dx ny dy') refl) ＝ ((dy *ℤ (dx *ℤ nx')) *ℤ dy') +ℤ ((dx *ℤ (dy *ℤ ny')) *ℤ dx') by ap-add-ℤ (ap-mul-ℤ (ap-mul-ℤ (refl {x = dy}) (p ∙ commutative-mul-ℤ nx' dx)) (refl {x = dy'})) (ap-mul-ℤ (ap-mul-ℤ (refl {x = dx}) (q ∙ commutative-mul-ℤ ny' dy)) (refl {x = dx'})) ＝ (((dy *ℤ dx) *ℤ nx') *ℤ dy') +ℤ (((dx *ℤ dy) *ℤ ny') *ℤ dx') by ap-add-ℤ (ap-mul-ℤ (inv (associative-mul-ℤ dy dx nx')) refl) (ap-mul-ℤ (inv (associative-mul-ℤ dx dy ny')) refl) ＝ ((nx' *ℤ (dy *ℤ dx)) *ℤ dy') +ℤ ((ny' *ℤ (dx *ℤ dy)) *ℤ dx') by ap-add-ℤ (ap-mul-ℤ (commutative-mul-ℤ (dy *ℤ dx) nx') refl) (ap-mul-ℤ (commutative-mul-ℤ (dx *ℤ dy) ny') refl) ＝ (nx' *ℤ ((dy *ℤ dx) *ℤ dy')) +ℤ (ny' *ℤ ((dx *ℤ dy) *ℤ dx')) by ap-add-ℤ (associative-mul-ℤ nx' (dy *ℤ dx) dy') (associative-mul-ℤ ny' (dx *ℤ dy) dx') ＝ (nx' *ℤ (dy' *ℤ (dy *ℤ dx))) +ℤ (ny' *ℤ (dx' *ℤ (dx *ℤ dy))) by ap-add-ℤ (ap-mul-ℤ (refl {x = nx'}) (commutative-mul-ℤ (dy *ℤ dx) dy')) (ap-mul-ℤ (refl {x = ny'}) (commutative-mul-ℤ (dx *ℤ dy) dx')) ＝ ((nx' *ℤ dy') *ℤ (dy *ℤ dx)) +ℤ ((ny' *ℤ dx') *ℤ (dx *ℤ dy)) by ap-add-ℤ (inv (associative-mul-ℤ nx' dy' (dy *ℤ dx))) (inv (associative-mul-ℤ ny' dx' (dx *ℤ dy))) ＝ ((nx' *ℤ dy') *ℤ (dx *ℤ dy)) +ℤ ((ny' *ℤ dx') *ℤ (dx *ℤ dy)) by ap-add-ℤ (ap-mul-ℤ (refl {x = nx' *ℤ dy'}) (commutative-mul-ℤ dy dx)) refl ＝ ((nx' *ℤ dy') +ℤ (ny' *ℤ dx')) *ℤ (dx *ℤ dy) by inv (right-distributive-mul-add-ℤ (nx' *ℤ dy') _ (dx *ℤ dy))
Unit laws
left-unit-law-add-fraction-ℤ : (k : fraction-ℤ) → sim-fraction-ℤ (zero-fraction-ℤ +fraction-ℤ k) k left-unit-law-add-fraction-ℤ (m , n , p) = ap-mul-ℤ (right-unit-law-mul-ℤ m) refl right-unit-law-add-fraction-ℤ : (k : fraction-ℤ) → sim-fraction-ℤ (k +fraction-ℤ zero-fraction-ℤ) k right-unit-law-add-fraction-ℤ (m , n , p) = ap-mul-ℤ ( ap-add-ℤ (right-unit-law-mul-ℤ m) refl ∙ right-unit-law-add-ℤ m) ( inv (right-unit-law-mul-ℤ n))
Addition is associative
associative-add-fraction-ℤ : (x y z : fraction-ℤ) → sim-fraction-ℤ ((x +fraction-ℤ y) +fraction-ℤ z) (x +fraction-ℤ (y +fraction-ℤ z)) associative-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = ap-mul-ℤ eq-num (inv (associative-mul-ℤ dx dy dz)) where eq-num : (((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)) ＝ (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) +ℤ (nz *ℤ dy)) *ℤ dx) eq-num = equational-reasoning (((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)) ＝ (((nx *ℤ dy) *ℤ dz) +ℤ ((ny *ℤ dx) *ℤ dz)) +ℤ (nz *ℤ (dx *ℤ dy)) by ap-add-ℤ (right-distributive-mul-add-ℤ (nx *ℤ dy) (ny *ℤ dx) dz) refl ＝ ((nx *ℤ dy) *ℤ dz) +ℤ (((ny *ℤ dx) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy))) by associative-add-ℤ ((nx *ℤ dy) *ℤ dz) ((ny *ℤ dx) *ℤ dz) _ ＝ (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dx) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy))) by ap-add-ℤ (associative-mul-ℤ nx dy dz) refl ＝ (nx *ℤ (dy *ℤ dz)) +ℤ ((ny *ℤ (dz *ℤ dx)) +ℤ (nz *ℤ (dy *ℤ dx))) by ap-add-ℤ (refl {x = nx *ℤ (dy *ℤ dz)}) (ap-add-ℤ (associative-mul-ℤ ny dx dz ∙ ap-mul-ℤ (refl {x = ny}) (commutative-mul-ℤ dx dz)) (ap-mul-ℤ (refl {x = nz}) (commutative-mul-ℤ dx dy))) ＝ (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) *ℤ dx) +ℤ ((nz *ℤ dy) *ℤ dx)) by ap-add-ℤ (refl {x = nx *ℤ (dy *ℤ dz)}) (inv (ap-add-ℤ ( associative-mul-ℤ ny dz dx) ( associative-mul-ℤ nz dy dx))) ＝ (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) +ℤ (nz *ℤ dy)) *ℤ dx) by ap-add-ℤ (refl {x = nx *ℤ (dy *ℤ dz)}) (inv (right-distributive-mul-add-ℤ (ny *ℤ dz) (nz *ℤ dy) dx))
Addition is commutative
commutative-add-fraction-ℤ : (x y : fraction-ℤ) → sim-fraction-ℤ (x +fraction-ℤ y) (y +fraction-ℤ x) commutative-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) = ap-mul-ℤ ( commutative-add-ℤ (nx *ℤ dy) (ny *ℤ dx)) ( commutative-mul-ℤ dy dx)